1
2
3
4 package net.sf.javabdd;
5
6 import java.util.Arrays;
7 import java.util.Collection;
8 import java.util.Collections;
9 import java.util.Comparator;
10 import java.util.Iterator;
11 import java.util.LinkedList;
12 import java.util.List;
13 import java.util.Random;
14 import java.util.StringTokenizer;
15 import java.io.BufferedReader;
16 import java.io.BufferedWriter;
17 import java.io.IOException;
18 import java.io.PrintStream;
19
20 /***
21 * <p>This is a 100% Java implementation of the BDD factory. It is based on
22 * the C source code for BuDDy. As such, the implementation is very ugly,
23 * but it works. Like BuDDy, it uses a reference counting scheme for garbage
24 * collection.</p>
25 *
26 * @author John Whaley
27 * @version $Id: JFactory.java 476 2007-03-06 06:08:40Z joewhaley $
28 */
29 public class JFactory extends BDDFactoryIntImpl {
30
31 /***** Options ****/
32
33 /***
34 * Flush the operation cache on every garbage collection. If this is false,
35 * we only clean the collected entries on every GC, rather than emptying the
36 * whole cache. For most problems, you should keep this set to true.
37 */
38 public static boolean FLUSH_CACHE_ON_GC = true;
39
40 static final boolean VERIFY_ASSERTIONS = false;
41 static final boolean CACHESTATS = false;
42 static final boolean SWAPCOUNT = false;
43
44 public static final String REVISION = "$Revision: 476 $";
45
46 public String getVersion() {
47 return "JFactory "+REVISION.substring(11, REVISION.length()-2);
48 }
49
50 private JFactory() { }
51
52
53
54
55 public static BDDFactory init(int nodenum, int cachesize) {
56 BDDFactory f = new JFactory();
57 f.initialize(nodenum, cachesize);
58 if (CACHESTATS) addShutdownHook(f);
59 return f;
60 }
61
62 static void addShutdownHook(final BDDFactory f) {
63 Runtime.getRuntime().addShutdownHook(new Thread() {
64 public void run() {
65 System.out.println(f.getCacheStats().toString());
66 }
67 });
68 }
69
70 boolean ZDD = false;
71
72 /***
73 * Implementation of BDDPairing used by JFactory.
74 */
75 class bddPair extends BDDPairing {
76 int[] result;
77 int last;
78 int id;
79 bddPair next;
80
81
82
83
84 public void set(int oldvar, int newvar) {
85 bdd_setpair(this, oldvar, newvar);
86 }
87
88
89
90 public void set(int oldvar, BDD newvar) {
91 bdd_setbddpair(this, oldvar, unwrap(newvar));
92 }
93
94
95
96 public void reset() {
97 bdd_resetpair(this);
98 }
99
100 public String toString() {
101 StringBuffer sb = new StringBuffer();
102 sb.append('{');
103 boolean any = false;
104 for (int i = 0; i < result.length; ++i) {
105 if (result[i] != (ZDD ? zdd_makenode(i, 0, 1):bdd_ithvar(bddlevel2var[i]))) {
106 if (any) sb.append(", ");
107 any = true;
108 sb.append(bddlevel2var[i]);
109 sb.append('=');
110
111
112
113 {
114 BDD b = makeBDD(result[i]);
115 sb.append(b);
116 b.free();
117 }
118 }
119 }
120 sb.append('}');
121 return sb.toString();
122 }
123 }
124
125
126
127
128 public BDDPairing makePair() {
129 bddPair p = new bddPair();
130 p.result = new int[bddvarnum];
131 int n;
132 for (n = 0; n < bddvarnum; n++)
133 if (ZDD)
134 p.result[n] = bdd_addref(zdd_makenode(n, 0, 1));
135 else
136 p.result[n] = bdd_ithvar(bddlevel2var[n]);
137
138 p.id = update_pairsid();
139 p.last = -1;
140
141 bdd_register_pair(p);
142 return p;
143 }
144
145
146
147 protected void addref_impl(int v) { bdd_addref(v); }
148 protected void delref_impl(int v) { bdd_delref(v); }
149 protected int zero_impl() { return BDDZERO; }
150 protected int one_impl() { return BDDONE; }
151 protected int universe_impl() { return univ; }
152 protected int invalid_bdd_impl() { return INVALID_BDD; }
153 protected int var_impl(int v) { return bdd_var(v); }
154 protected int level_impl(int v) { return LEVEL(v); }
155 protected int low_impl(int v) { return bdd_low(v); }
156 protected int high_impl(int v) { return bdd_high(v); }
157 protected int ithVar_impl(int var) { return bdd_ithvar(var); }
158 protected int nithVar_impl(int var) { return bdd_nithvar(var); }
159
160 protected int makenode_impl(int lev, int lo, int hi) {
161 if (ZDD)
162 return zdd_makenode(lev, lo, hi);
163 else
164 return bdd_makenode(lev, lo, hi);
165 }
166 protected int ite_impl(int v1, int v2, int v3) { return bdd_ite(v1, v2, v3); }
167 protected int apply_impl(int v1, int v2, BDDOp opr) { return bdd_apply(v1, v2, opr.id); }
168 protected int not_impl(int v1) { return bdd_not(v1); }
169 protected int applyAll_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appall(v1, v2, opr.id, v3); }
170 protected int applyEx_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appex(v1, v2, opr.id, v3); }
171 protected int applyUni_impl(int v1, int v2, BDDOp opr, int v3) { return bdd_appuni(v1, v2, opr.id, v3); }
172 protected int compose_impl(int v1, int v2, int var) { return bdd_compose(v1, v2, var); }
173 protected int constrain_impl(int v1, int v2) { return bdd_constrain(v1, v2); }
174 protected int restrict_impl(int v1, int v2) { return bdd_restrict(v1, v2); }
175 protected int simplify_impl(int v1, int v2) { return bdd_simplify(v1, v2); }
176 protected int support_impl(int v) { return bdd_support(v); }
177 protected int exist_impl(int v1, int v2) { return bdd_exist(v1, v2); }
178 protected int forAll_impl(int v1, int v2) { return bdd_forall(v1, v2); }
179 protected int unique_impl(int v1, int v2) { return bdd_unique(v1, v2); }
180 protected int fullSatOne_impl(int v) { return bdd_fullsatone(v); }
181
182 protected int replace_impl(int v, BDDPairing p) { return bdd_replace(v, (bddPair)p); }
183 protected int veccompose_impl(int v, BDDPairing p) { return bdd_veccompose(v, (bddPair)p); }
184
185 protected int nodeCount_impl(int v) { return bdd_nodecount(v); }
186 protected double pathCount_impl(int v) { return bdd_pathcount(v); }
187 protected double satCount_impl(int v) { return bdd_satcount(v); }
188 protected int satOne_impl(int v) { return bdd_satone(v); }
189 protected int satOne_impl2(int v1, int v2, boolean pol) { return bdd_satoneset(v1, v2, pol); }
190 protected int nodeCount_impl2(int[] v) { return bdd_anodecount(v); }
191 protected int[] varProfile_impl(int v) { return bdd_varprofile(v); }
192 protected void printTable_impl(int v) { bdd_fprinttable(System.out, v); }
193
194
195
196 protected void initialize(int initnodesize, int cs) { bdd_init(initnodesize, cs); }
197 public void addVarBlock(int first, int last, boolean fixed) { bdd_intaddvarblock(first, last, fixed); }
198 public void varBlockAll() { bdd_varblockall(); }
199 public void clearVarBlocks() { bdd_clrvarblocks(); }
200 public void printOrder() { bdd_fprintorder(System.out); }
201 public int getNodeTableSize() { return bdd_getallocnum(); }
202 public int setNodeTableSize(int size) { return bdd_setallocnum(size); }
203 public int setCacheSize(int v) { return bdd_setcachesize(v); }
204 public boolean isZDD() { return ZDD; }
205 public boolean isInitialized() { return bddrunning; }
206 public void done() { super.done(); bdd_done(); }
207 public void setError(int code) { bdderrorcond = code; }
208 public void clearError() { bdderrorcond = 0; }
209 public int setMaxNodeNum(int size) { return bdd_setmaxnodenum(size); }
210 public double setMinFreeNodes(double x) { return bdd_setminfreenodes((int)(x * 100.)) / 100.; }
211 public int setMaxIncrease(int x) { return bdd_setmaxincrease(x); }
212 public double setIncreaseFactor(double x) { return bdd_setincreasefactor(x); }
213 public int getNodeNum() { return bdd_getnodenum(); }
214 public int getCacheSize() { return cachesize; }
215 public int reorderGain() { return bdd_reorder_gain(); }
216 public void printStat() { bdd_fprintstat(System.out); }
217 public double setCacheRatio(double x) { return bdd_setcacheratio((int)x); }
218 public int varNum() { return bdd_varnum(); }
219 public int setVarNum(int num) { return bdd_setvarnum(num); }
220 public void printAll() { bdd_fprintall(System.out); }
221 public BDD load(BufferedReader in, int[] translate) throws IOException { return makeBDD(bdd_load(in, translate)); }
222 public void save(BufferedWriter out, BDD b) throws IOException { bdd_save(out, unwrap(b)); }
223 public void setVarOrder(int[] neworder) { bdd_setvarorder(neworder); }
224 public int level2Var(int level) { return bddlevel2var[level]; }
225 public int var2Level(int var) { return bddvar2level[var]; }
226 public int getReorderTimes() { return bddreordertimes; }
227 public void disableReorder() { bdd_disable_reorder(); }
228 public void enableReorder() { bdd_enable_reorder(); }
229 public int reorderVerbose(int v) { return bdd_reorder_verbose(v); }
230 public void reorder(ReorderMethod m) { bdd_reorder(m.id); }
231 public void autoReorder(ReorderMethod method) { bdd_autoreorder(method.id); }
232 public void autoReorder(ReorderMethod method, int max) { bdd_autoreorder_times(method.id, max); }
233 public void swapVar(int v1, int v2) { bdd_swapvar(v1, v2); }
234
235 public ReorderMethod getReorderMethod() {
236 switch (bddreordermethod) {
237 case BDD_REORDER_NONE :
238 return REORDER_NONE;
239 case BDD_REORDER_WIN2 :
240 return REORDER_WIN2;
241 case BDD_REORDER_WIN2ITE :
242 return REORDER_WIN2ITE;
243 case BDD_REORDER_WIN3 :
244 return REORDER_WIN3;
245 case BDD_REORDER_WIN3ITE :
246 return REORDER_WIN3ITE;
247 case BDD_REORDER_SIFT :
248 return REORDER_SIFT;
249 case BDD_REORDER_SIFTITE :
250 return REORDER_SIFTITE;
251 case BDD_REORDER_RANDOM :
252 return REORDER_RANDOM;
253 default :
254 throw new BDDException();
255 }
256 }
257
258
259
260 public void validateAll() { bdd_validate_all(); }
261 public void validateBDD(BDD b) { bdd_validate(unwrap(b)); }
262
263 public JFactory cloneFactory() {
264 JFactory INSTANCE = new JFactory();
265 if (applycache != null)
266 INSTANCE.applycache = this.applycache.copy();
267 if (itecache != null)
268 INSTANCE.itecache = this.itecache.copy();
269 if (quantcache != null)
270 INSTANCE.quantcache = this.quantcache.copy();
271 INSTANCE.appexcache = this.appexcache.copy();
272 if (replacecache != null)
273 INSTANCE.replacecache = this.replacecache.copy();
274 if (misccache != null)
275 INSTANCE.misccache = this.misccache.copy();
276 if (countcache != null)
277 INSTANCE.countcache = this.countcache.copy();
278
279 INSTANCE.rng = new Random();
280 INSTANCE.verbose = this.verbose;
281 INSTANCE.cachestats.copyFrom(this.cachestats);
282
283 INSTANCE.bddrunning = this.bddrunning;
284 INSTANCE.bdderrorcond = this.bdderrorcond;
285 INSTANCE.bddnodesize = this.bddnodesize;
286 INSTANCE.bddmaxnodesize = this.bddmaxnodesize;
287 INSTANCE.bddmaxnodeincrease = this.bddmaxnodeincrease;
288 INSTANCE.bddfreepos = this.bddfreepos;
289 INSTANCE.bddfreenum = this.bddfreenum;
290 INSTANCE.bddproduced = this.bddproduced;
291 INSTANCE.bddvarnum = this.bddvarnum;
292
293 INSTANCE.gbcollectnum = this.gbcollectnum;
294 INSTANCE.cachesize = this.cachesize;
295 INSTANCE.gbcclock = this.gbcclock;
296 INSTANCE.usednodes_nextreorder = this.usednodes_nextreorder;
297
298 INSTANCE.bddrefstacktop = this.bddrefstacktop;
299 INSTANCE.bddresized = this.bddresized;
300 INSTANCE.minfreenodes = this.minfreenodes;
301 INSTANCE.bddnodes = new int[this.bddnodes.length];
302 System.arraycopy(this.bddnodes, 0, INSTANCE.bddnodes, 0, this.bddnodes.length);
303 INSTANCE.bddrefstack = new int[this.bddrefstack.length];
304 System.arraycopy(this.bddrefstack, 0, INSTANCE.bddrefstack, 0, this.bddrefstack.length);
305 INSTANCE.bddvar2level = new int[this.bddvar2level.length];
306 System.arraycopy(this.bddvar2level, 0, INSTANCE.bddvar2level, 0, this.bddvar2level.length);
307 INSTANCE.bddlevel2var = new int[this.bddlevel2var.length];
308 System.arraycopy(this.bddlevel2var, 0, INSTANCE.bddlevel2var, 0, this.bddlevel2var.length);
309 INSTANCE.bddvarset = new int[this.bddvarset.length];
310 System.arraycopy(this.bddvarset, 0, INSTANCE.bddvarset, 0, this.bddvarset.length);
311
312 INSTANCE.domain = new BDDDomain[this.domain.length];
313 for (int i = 0; i < INSTANCE.domain.length; ++i) {
314 INSTANCE.domain[i] = INSTANCE.createDomain(i, this.domain[i].realsize);
315 }
316 return INSTANCE;
317 }
318
319 /***
320 * Use this function to translate BDD's from a JavaFactory into its clone.
321 * This will only work immediately after cloneFactory() is called, and
322 * before any other BDD operations are performed.
323 *
324 * @param that BDD in old factory
325 * @return a BDD in the new factory
326 */
327 public BDD copyNode(BDD that) {
328 return makeBDD(unwrap(that));
329 }
330
331 public void reverseAllDomains() {
332 reorder_init();
333 for (int i = 0; i < fdvarnum; ++i) {
334 reverseDomain0(domain[i]);
335 }
336 reorder_done();
337 }
338
339 public void reverseDomain(BDDDomain d) {
340 reorder_init();
341 reverseDomain0(d);
342 reorder_done();
343 }
344
345 protected void reverseDomain0(BDDDomain d) {
346 int n = d.varNum();
347 BddTree[] trees = new BddTree[n];
348 int v = d.ivar[0];
349 addVarBlock(v, v, true);
350 trees[0] = getBlock(vartree, v, v);
351 BddTree parent = getParent(trees[0]);
352 for (int i = 1; i < n; ++i) {
353 v = d.ivar[i];
354 addVarBlock(v, v, true);
355 trees[i] = getBlock(vartree, v, v);
356 BddTree parent2 = getParent(trees[i]);
357 if (parent != parent2) {
358 throw new BDDException();
359 }
360 }
361 for (int i = 0; i < n; ++i) {
362 for (int j = i + 1; j < n; ++j) {
363 blockdown(trees[i]);
364 }
365 }
366 BddTree newchild = trees[n-1];
367 while (newchild.prev != null) newchild = newchild.prev;
368 if (parent == null) vartree = newchild;
369 else parent.nextlevel = newchild;
370 }
371
372 public void setVarOrder(String ordering) {
373 List result = new LinkedList();
374 int nDomains = numberOfDomains();
375 StringTokenizer st = new StringTokenizer(ordering, "x_", true);
376 boolean[] done = new boolean[nDomains];
377 List last = null;
378 for (int i=0; ; ++i) {
379 String s = st.nextToken();
380 BDDDomain d;
381 for (int j=0; ; ++j) {
382 if (j == nDomains)
383 throw new BDDException("bad domain: "+s);
384 d = getDomain(j);
385 if (s.equals(d.getName())) break;
386 }
387 if (done[d.getIndex()])
388 throw new BDDException("duplicate domain: "+s);
389 done[d.getIndex()] = true;
390 if (last != null) last.add(d);
391 if (st.hasMoreTokens()) {
392 s = st.nextToken();
393 if (s.equals("x")) {
394 if (last == null) {
395 last = new LinkedList();
396 last.add(d);
397 result.add(last);
398 }
399 } else if (s.equals("_")) {
400 if (last == null) {
401 result.add(d);
402 }
403 last = null;
404 } else {
405 throw new BDDException("bad token: "+s);
406 }
407 } else {
408 if (last == null) {
409 result.add(d);
410 }
411 break;
412 }
413 }
414
415 for (int i=0; i<done.length; ++i) {
416 if (!done[i]) {
417 throw new BDDException("missing domain #"+i+": "+getDomain(i));
418 }
419 }
420
421 setVarOrder(result);
422 }
423
424 /***
425 * <p>Set the variable order to be the given list of domains.</p>
426 *
427 * @param domains domain order
428 */
429 public void setVarOrder(List domains) {
430 BddTree[] my_vartree = new BddTree[fdvarnum];
431 boolean[] interleaved = new boolean[fdvarnum];
432 int k = 0;
433 for (Iterator i = domains.iterator(); i.hasNext(); ) {
434 Object o = i.next();
435 Collection c;
436 if (o instanceof BDDDomain) c = Collections.singleton(o);
437 else c = (Collection) o;
438 for (Iterator j = c.iterator(); j.hasNext(); ) {
439 BDDDomain d = (BDDDomain) j.next();
440 int low = d.ivar[0];
441 int high = d.ivar[d.ivar.length-1];
442 bdd_intaddvarblock(low, high, false);
443 BddTree b = getBlock(vartree, low, high);
444 my_vartree[k] = b;
445 interleaved[k] = j.hasNext();
446 k++;
447 }
448 }
449 if (k <= 1) return;
450 BddTree parent = getParent(my_vartree[0]);
451 for (int i = 0; i < k; ++i) {
452 if (parent != getParent(my_vartree[i])) {
453 throw new BDDException("var block "+my_vartree[i].firstVar+".."+my_vartree[i].lastVar+" is in wrong place in tree");
454 }
455 }
456 reorder_init();
457 BddTree prev = null; boolean prev_interleaved = false;
458 for (int i = 0; i < k; ++i) {
459 BddTree t = my_vartree[i];
460 while (t.prev != prev) {
461 blockdown(t.prev);
462 }
463 boolean inter = interleaved[i];
464 if (prev_interleaved) {
465 blockinterleave(t.prev);
466
467 prev = t.prev;
468 } else {
469 prev = t;
470 }
471 prev_interleaved = inter;
472 }
473 BddTree newchild = my_vartree[0];
474 if (VERIFY_ASSERTIONS) _assert(newchild.prev == null);
475
476 if (parent == null) vartree = newchild;
477 else parent.nextlevel = newchild;
478 reorder_done();
479 }
480
481 protected BddTree getParent(BddTree child) {
482 for (BddTree p = vartree; p != null; p = p.next) {
483 if (p == child) return null;
484 BddTree q = getParent(p, child);
485 if (q != null) return q;
486 }
487 throw new BDDException("Cannot find tree node "+child);
488 }
489
490 protected BddTree getParent(BddTree parent, BddTree child) {
491 if (parent.nextlevel == null) return null;
492 for (BddTree p = parent.nextlevel; p != null; p = p.next) {
493 if (p == child) return parent;
494 BddTree q = getParent(p, child);
495 if (q != null) return q;
496 }
497 return null;
498 }
499
500 protected BddTree getBlock(BddTree t, int low, int high) {
501 if (t == null) return null;
502 for (BddTree p = t; p != null; p = p.next) {
503 if (p.firstVar == low && p.lastVar == high) return p;
504 BddTree q = getBlock(p.nextlevel, low, high);
505 if (q != null) return q;
506 }
507 return null;
508 }
509
510 /****** IMPLEMENTATION BELOW *****/
511
512 static final int REF_MASK = 0xFFC00000;
513 static final int MARK_MASK = 0x00200000;
514 static final int LEV_MASK = 0x001FFFFF;
515 static final int MAXVAR = LEV_MASK;
516 static final int INVALID_BDD = -1;
517
518 static final int REF_INC = 0x00400000;
519
520 static final int offset__refcou_and_level = 0;
521 static final int offset__low = 1;
522 static final int offset__high = 2;
523 static final int offset__hash = 3;
524 static final int offset__next = 4;
525 static final int __node_size = 5;
526
527 private final boolean HASREF(int node) {
528 boolean r = (bddnodes[node*__node_size + offset__refcou_and_level] & REF_MASK) != 0;
529 return r;
530 }
531
532 private final void SETMAXREF(int node) {
533 bddnodes[node*__node_size + offset__refcou_and_level] |= REF_MASK;
534 }
535
536 private final void CLEARREF(int node) {
537 bddnodes[node*__node_size + offset__refcou_and_level] &= ~REF_MASK;
538 }
539
540 private final void INCREF(int node) {
541 if ((bddnodes[node*__node_size + offset__refcou_and_level] & REF_MASK) != REF_MASK)
542 bddnodes[node*__node_size + offset__refcou_and_level] += REF_INC;
543 }
544
545 private final void DECREF(int node) {
546 int rc = bddnodes[node*__node_size + offset__refcou_and_level] & REF_MASK;
547 if (rc != REF_MASK && rc != 0)
548 bddnodes[node*__node_size + offset__refcou_and_level] -= REF_INC;
549 }
550
551 private final int GETREF(int node) {
552 return bddnodes[node*__node_size + offset__refcou_and_level] >>> 22;
553 }
554
555 private final int LEVEL(int node) {
556 return bddnodes[node*__node_size + offset__refcou_and_level] & LEV_MASK;
557 }
558
559 private final int LEVELANDMARK(int node) {
560 return bddnodes[node*__node_size + offset__refcou_and_level] & (LEV_MASK | MARK_MASK);
561 }
562
563 private final void SETLEVEL(int node, int val) {
564 if (VERIFY_ASSERTIONS) _assert(val == (val & LEV_MASK));
565 bddnodes[node*__node_size + offset__refcou_and_level] &= ~LEV_MASK;
566 bddnodes[node*__node_size + offset__refcou_and_level] |= val;
567 }
568
569 private final void SETLEVELANDMARK(int node, int val) {
570 if (VERIFY_ASSERTIONS) _assert(val == (val & (LEV_MASK | MARK_MASK)));
571 bddnodes[node*__node_size + offset__refcou_and_level] &= ~(LEV_MASK | MARK_MASK);
572 bddnodes[node*__node_size + offset__refcou_and_level] |= val;
573 }
574
575 private final void SETMARK(int n) {
576 bddnodes[n*__node_size + offset__refcou_and_level] |= MARK_MASK;
577 }
578
579 private final void UNMARK(int n) {
580 bddnodes[n*__node_size + offset__refcou_and_level] &= ~MARK_MASK;
581 }
582
583 private final boolean MARKED(int n) {
584 return (bddnodes[n*__node_size + offset__refcou_and_level] & MARK_MASK) != 0;
585 }
586
587 private final int LOW(int r) {
588 return bddnodes[r*__node_size + offset__low];
589 }
590
591 private final void SETLOW(int r, int v) {
592 bddnodes[r*__node_size + offset__low] = v;
593 }
594
595 private final int HIGH(int r) {
596 return bddnodes[r*__node_size + offset__high];
597 }
598
599 private final void SETHIGH(int r, int v) {
600 bddnodes[r*__node_size + offset__high] = v;
601 }
602
603 private final int HASH(int r) {
604 return bddnodes[r*__node_size + offset__hash];
605 }
606
607 private final void SETHASH(int r, int v) {
608 bddnodes[r*__node_size + offset__hash] = v;
609 }
610
611 private final int NEXT(int r) {
612 return bddnodes[r*__node_size + offset__next];
613 }
614
615 private final void SETNEXT(int r, int v) {
616 bddnodes[r*__node_size + offset__next] = v;
617 }
618
619 private final int VARr(int n) {
620 return LEVELANDMARK(n);
621 }
622
623 void SETVARr(int n, int val) {
624 SETLEVELANDMARK(n, val);
625 }
626
627 static final void _assert(boolean b) {
628 if (!b)
629 throw new InternalError();
630 }
631
632 private abstract static class BddCacheData {
633 int a, b, c;
634 abstract BddCacheData copy();
635 }
636
637 private static class BddCacheDataI extends BddCacheData {
638 int res;
639 BddCacheData copy() {
640 BddCacheDataI that = new BddCacheDataI();
641 that.a = this.a;
642 that.b = this.b;
643 that.c = this.c;
644 that.res = this.res;
645 return that;
646 }
647 }
648
649 private static class BddCacheDataD extends BddCacheData {
650 double dres;
651 BddCacheData copy() {
652 BddCacheDataD that = new BddCacheDataD();
653 that.a = this.a;
654 that.b = this.b;
655 that.c = this.c;
656 that.dres = this.dres;
657 return that;
658 }
659 }
660
661 private static class BddCache {
662 BddCacheData table[];
663 int tablesize;
664
665 BddCache copy() {
666 BddCache that = new BddCache();
667 boolean is_d = this.table instanceof BddCacheDataD[];
668 if (is_d) {
669 that.table = new BddCacheDataD[this.table.length];
670 } else {
671 that.table = new BddCacheDataI[this.table.length];
672 }
673 that.tablesize = this.tablesize;
674 for (int i = 0; i < table.length; ++i) {
675 that.table[i] = this.table[i].copy();
676 }
677 return that;
678 }
679 }
680
681 private static class JavaBDDException extends BDDException {
682 /***
683 * Version ID for serialization.
684 */
685 private static final long serialVersionUID = 3257289144995952950L;
686
687 public JavaBDDException(int x) {
688 super(errorstrings[-x]);
689 }
690 }
691
692 private static class ReorderException extends RuntimeException {
693 /***
694 * Version ID for serialization.
695 */
696 private static final long serialVersionUID = 3256727264505772345L;
697 }
698
699 static final int bddtrue = 1;
700 static final int bddfalse = 0;
701
702 static final int BDDONE = 1;
703 static final int BDDZERO = 0;
704
705 boolean bddrunning; /package-summary.html">initialized */
706 int bdderrorcond;
707 int bddnodesize;
708 int bddmaxnodesize;
709 int bddmaxnodeincrease;
710 int[] bddnodes;
711 int bddfreepos;
712 int bddfreenum;
713 int bddproduced;
714 int bddvarnum;
715 int[] bddrefstack;
716 int bddrefstacktop;
717 int[] bddvar2level;
718 int[] bddlevel2var;
719 boolean bddresized;
720
721 int minfreenodes = 20;
722
723
724
725 int[] bddvarset;
726 int univ = 1;
727 int gbcollectnum;
728 int cachesize;
729 long gbcclock;
730 int usednodes_nextreorder;
731
732 static final int BDD_MEMORY = (-1);
733 static final int BDD_VAR = (-2);
734 static final int BDD_RANGE = (-3);
735 static final int BDD_DEREF = (-4);
736 static final int BDD_RUNNING = (-5);
737 static final int BDD_FILE = (-6);
738 static final int BDD_FORMAT = (-7);
739 static final int BDD_ORDER = (-8);
740 static final int BDD_BREAK = (-9);
741 static final int BDD_VARNUM = (-10);
742 static final int BDD_NODES = (-11);
743
744 static final int BDD_OP = (-12);
745 static final int BDD_VARSET = (-13);
746 static final int BDD_VARBLK = (-14);
747 static final int BDD_DECVNUM = (-15);
748 static final int BDD_REPLACE = (-16);
749 static final int BDD_NODENUM = (-17);
750 static final int BDD_ILLBDD = (-18);
751 static final int BDD_SIZE = (-19);
752
753 static final int BVEC_SIZE = (-20);
754 static final int BVEC_SHIFT = (-21);
755 static final int BVEC_DIVZERO = (-22);
756
757 static final int BDD_ERRNUM = 24;
758
759
760 static String errorstrings[] =
761 {
762 "",
763 "Out of memory",
764 "Unknown variable",
765 "Value out of range",
766 "Unknown BDD root dereferenced",
767 "bdd_init() called twice",
768 "File operation failed",
769 "Incorrect file format",
770 "Variables not in ascending order",
771 "User called break",
772 "Mismatch in size of variable sets",
773 "Cannot allocate fewer nodes than already in use",
774 "Unknown operator",
775 "Illegal variable set",
776 "Bad variable block operation",
777 "Trying to decrease the number of variables",
778 "Trying to replace with variables already in the bdd",
779 "Number of nodes reached user defined maximum",
780 "Unknown BDD - was not in node table",
781 "Bad size argument",
782 "Mismatch in bitvector size",
783 "Illegal shift-left/right parameter",
784 "Division by zero" };
785
786 static final int DEFAULTMAXNODEINC = 10000000;
787
788
789
790 static final int PAIR(int a, int b) {
791
792 return ((a + b) * (a + b + 1) / 2 + a);
793 }
794 static final int TRIPLE(int a, int b, int c) {
795
796 return (PAIR(c, PAIR(a, b)));
797 }
798
799 final int NODEHASH(int lvl, int l, int h) {
800 return Math.abs(TRIPLE(lvl, l, h) % bddnodesize);
801 }
802
803 int bdd_ithvar(int var) {
804 if (var < 0 || var >= bddvarnum) {
805 bdd_error(BDD_VAR);
806 return bddfalse;
807 }
808
809 return bddvarset[var * 2];
810 }
811
812 int bdd_nithvar(int var) {
813 if (var < 0 || var >= bddvarnum) {
814 bdd_error(BDD_VAR);
815 return bddfalse;
816 }
817
818 return bddvarset[var * 2 + 1];
819 }
820
821 int bdd_varnum() {
822 return bddvarnum;
823 }
824
825 static int bdd_error(int v) {
826 throw new JavaBDDException(v);
827 }
828
829 static boolean ISZERO(int r) {
830 return r == bddfalse;
831 }
832
833 static boolean ISONE(int r) {
834 return r == bddtrue;
835 }
836
837 static boolean ISCONST(int r) {
838
839 return r < 2;
840 }
841
842 void CHECK(int r) {
843 if (!bddrunning)
844 bdd_error(BDD_RUNNING);
845 else if (r < 0 || r >= bddnodesize)
846 bdd_error(BDD_ILLBDD);
847 else if (r >= 2 && LOW(r) == INVALID_BDD)
848 bdd_error(BDD_ILLBDD);
849 }
850 void CHECKa(int r, int x) {
851 CHECK(r);
852 }
853
854 int bdd_var(int root) {
855 CHECK(root);
856 if (root < 2)
857 bdd_error(BDD_ILLBDD);
858
859 return (bddlevel2var[LEVEL(root)]);
860 }
861
862 int bdd_low(int root) {
863 CHECK(root);
864 if (root < 2)
865 return bdd_error(BDD_ILLBDD);
866
867 return (LOW(root));
868 }
869
870 int bdd_high(int root) {
871 CHECK(root);
872 if (root < 2)
873 return bdd_error(BDD_ILLBDD);
874
875 return (HIGH(root));
876 }
877
878 void checkresize() {
879 if (bddresized)
880 bdd_operator_noderesize();
881 bddresized = false;
882 }
883
884 static final int NOTHASH(int r) {
885 return r;
886 }
887 static final int APPLYHASH(int l, int r, int op) {
888 return TRIPLE(l, r, op);
889 }
890 static final int ITEHASH(int f, int g, int h) {
891 return TRIPLE(f, g, h);
892 }
893 static final int RESTRHASH(int r, int var) {
894 return PAIR(r, var);
895 }
896 static final int CONSTRAINHASH(int f, int c) {
897 return PAIR(f, c);
898 }
899 static final int QUANTHASH(int r) {
900 return r;
901 }
902 static final int REPLACEHASH(int r) {
903 return r;
904 }
905 static final int VECCOMPOSEHASH(int f) {
906 return f;
907 }
908 static final int COMPOSEHASH(int f, int g) {
909 return PAIR(f, g);
910 }
911 static final int SATCOUHASH(int r) {
912 return r;
913 }
914 static final int PATHCOUHASH(int r) {
915 return r;
916 }
917 static final int APPEXHASH(int l, int r, int op) {
918 return PAIR(l, r);
919 }
920
921 static final double M_LN2 = 0.69314718055994530942;
922
923 static double log1p(double a) {
924 return Math.log(1.0 + a);
925 }
926
927 final boolean INVARSET(int a) {
928 return (quantvarset[a] == quantvarsetID);
929 }
930 final boolean INSVARSET(int a) {
931 return Math.abs(quantvarset[a]) == quantvarsetID;
932 }
933
934 static final int bddop_and = 0;
935 static final int bddop_xor = 1;
936 static final int bddop_or = 2;
937 static final int bddop_nand = 3;
938 static final int bddop_nor = 4;
939 static final int bddop_imp = 5;
940 static final int bddop_biimp = 6;
941 static final int bddop_diff = 7;
942 static final int bddop_less = 8;
943 static final int bddop_invimp = 9;
944
945
946 static final int bddop_not = 10;
947 static final int bddop_simplify = 11;
948
949 int bdd_not(int r) {
950 int res;
951 int numReorder = 1;
952 CHECKa(r, bddfalse);
953
954 if (applycache == null) applycache = BddCacheI_init(cachesize);
955 again : for (;;) {
956 try {
957 INITREF();
958
959 if (numReorder == 0) bdd_disable_reorder();
960 if (ZDD) res = zdiff_rec(univ, r);
961 else res = not_rec(r);
962 if (numReorder == 0) bdd_enable_reorder();
963 } catch (ReorderException x) {
964 bdd_checkreorder();
965 numReorder--;
966 continue again;
967 }
968 break;
969 }
970
971 checkresize();
972 return res;
973 }
974
975 int not_rec(int r) {
976 BddCacheDataI entry;
977 int res;
978
979 if (ISCONST(r))
980 return 1 - r;
981
982 entry = BddCache_lookupI(applycache, NOTHASH(r));
983
984 if (entry.a == r && entry.c == bddop_not) {
985 if (CACHESTATS)
986 cachestats.opHit++;
987 return entry.res;
988 }
989 if (CACHESTATS)
990 cachestats.opMiss++;
991
992 PUSHREF(not_rec(LOW(r)));
993 PUSHREF(not_rec(HIGH(r)));
994 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
995 POPREF(2);
996
997 entry.a = r;
998 entry.c = bddop_not;
999 entry.res = res;
1000
1001 return res;
1002 }
1003
1004 int bdd_ite(int f, int g, int h) {
1005 int res;
1006 int numReorder = 1;
1007
1008 CHECKa(f, bddfalse);
1009 CHECKa(g, bddfalse);
1010 CHECKa(h, bddfalse);
1011
1012 if (applycache == null) applycache = BddCacheI_init(cachesize);
1013 if (itecache == null) itecache = BddCacheI_init(cachesize);
1014
1015 again : for (;;) {
1016 try {
1017 INITREF();
1018
1019 if (numReorder == 0) bdd_disable_reorder();
1020 res = ZDD ? zite_rec(f, g, h) : ite_rec(f, g, h);
1021 if (numReorder == 0) bdd_enable_reorder();
1022 } catch (ReorderException x) {
1023 bdd_checkreorder();
1024 numReorder--;
1025 continue again;
1026 }
1027 break;
1028 }
1029
1030 checkresize();
1031 return res;
1032 }
1033
1034 int ite_rec(int f, int g, int h) {
1035 BddCacheDataI entry;
1036 int res;
1037
1038 if (ISONE(f))
1039 return g;
1040 if (ISZERO(f))
1041 return h;
1042 if (g == h)
1043 return g;
1044 if (ISONE(g) && ISZERO(h))
1045 return f;
1046 if (ISZERO(g) && ISONE(h))
1047 return not_rec(f);
1048
1049 entry = BddCache_lookupI(itecache, ITEHASH(f, g, h));
1050 if (entry.a == f && entry.b == g && entry.c == h) {
1051 if (CACHESTATS)
1052 cachestats.opHit++;
1053 return entry.res;
1054 }
1055 if (CACHESTATS)
1056 cachestats.opMiss++;
1057
1058 if (LEVEL(f) == LEVEL(g)) {
1059 if (LEVEL(f) == LEVEL(h)) {
1060 PUSHREF(ite_rec(LOW(f), LOW(g), LOW(h)));
1061 PUSHREF(ite_rec(HIGH(f), HIGH(g), HIGH(h)));
1062 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
1063 } else if (LEVEL(f) < LEVEL(h)) {
1064 PUSHREF(ite_rec(LOW(f), LOW(g), h));
1065 PUSHREF(ite_rec(HIGH(f), HIGH(g), h));
1066 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
1067 } else
1068 PUSHREF(ite_rec(f, g, LOW(h)));
1069 PUSHREF(ite_rec(f, g, HIGH(h)));
1070 res = bdd_makenode(LEVEL(h), READREF(2), READREF(1));
1071 }
1072 } else if (LEVEL(f) < LEVEL(g)) {
1073 if (LEVEL(f) == LEVEL(h)) {
1074 PUSHREF(ite_rec(LOW(f), g, LOW(h)));
1075 PUSHREF(ite_rec(HIGH(f), g, HIGH(h)));
1076 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
1077 } else if (LEVEL(f) < LEVEL(h)) {
1078 PUSHREF(ite_rec(LOW(f), g, h));
1079 PUSHREF(ite_rec(HIGH(f), g, h));
1080 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
1081 } else
1082 PUSHREF(ite_rec(f, g, LOW(h)));
1083 PUSHREF(ite_rec(f, g, HIGH(h)));
1084 res = bdd_makenode(LEVEL(h), READREF(2), READREF(1));
1085 }
1086 } else
1087 if (LEVEL(g) == LEVEL(h)) {
1088 PUSHREF(ite_rec(f, LOW(g), LOW(h)));
1089 PUSHREF(ite_rec(f, HIGH(g), HIGH(h)));
1090 res = bdd_makenode(LEVEL(g), READREF(2), READREF(1));
1091 } else if (LEVEL(g) < LEVEL(h)) {
1092 PUSHREF(ite_rec(f, LOW(g), h));
1093 PUSHREF(ite_rec(f, HIGH(g), h));
1094 res = bdd_makenode(LEVEL(g), READREF(2), READREF(1));
1095 } else
1096 PUSHREF(ite_rec(f, g, LOW(h)));
1097 PUSHREF(ite_rec(f, g, HIGH(h)));
1098 res = bdd_makenode(LEVEL(h), READREF(2), READREF(1));
1099 }
1100 }
1101
1102 POPREF(2);
1103
1104 entry.a = f;
1105 entry.b = g;
1106 entry.c = h;
1107 entry.res = res;
1108
1109 return res;
1110 }
1111
1112 int zite_rec(int f, int g, int h) {
1113 BddCacheDataI entry;
1114 int res;
1115
1116 if (ISONE(f))
1117 return g;
1118 if (ISZERO(f))
1119 return h;
1120 if (g == h)
1121 return g;
1122 if (ISONE(g) && ISZERO(h))
1123 return f;
1124 if (ISZERO(g) && ISONE(h))
1125 return zdiff_rec(univ, f);
1126
1127 int v = Math.min(LEVEL(g), LEVEL(h));
1128 if (LEVEL(f) < v)
1129 return zite_rec(LOW(f), g, h);
1130
1131 entry = BddCache_lookupI(itecache, ITEHASH(f, g, h));
1132 if (entry.a == f && entry.b == g && entry.c == h) {
1133 if (CACHESTATS)
1134 cachestats.opHit++;
1135 return entry.res;
1136 }
1137 if (CACHESTATS)
1138 cachestats.opMiss++;
1139
1140 if (LEVEL(f) == LEVEL(g)) {
1141 if (LEVEL(f) == LEVEL(h)) {
1142 PUSHREF(zite_rec(LOW(f), LOW(g), LOW(h)));
1143 PUSHREF(zite_rec(HIGH(f), HIGH(g), HIGH(h)));
1144 res = zdd_makenode(LEVEL(f), READREF(2), READREF(1));
1145 POPREF(2);
1146 } else if (LEVEL(f) < LEVEL(h)) {
1147 PUSHREF(zite_rec(LOW(f), LOW(g), h));
1148 PUSHREF(zite_rec(HIGH(f), HIGH(g), 0));
1149 res = zdd_makenode(LEVEL(f), READREF(2), READREF(1));
1150 POPREF(2);
1151 } else
1152 PUSHREF(zite_rec(f, g, LOW(h)));
1153 res = zdd_makenode(LEVEL(h), HIGH(h), READREF(1));
1154 POPREF(1);
1155 }
1156 } else if (LEVEL(f) < LEVEL(g)) {
1157 if (LEVEL(f) == LEVEL(h)) {
1158 PUSHREF(zite_rec(LOW(f), g, LOW(h)));
1159 PUSHREF(zite_rec(HIGH(f), 0, HIGH(h)));
1160 res = zdd_makenode(LEVEL(f), READREF(2), READREF(1));
1161 POPREF(2);
1162 } else if (LEVEL(f) < LEVEL(h)) {
1163 res = zite_rec(LOW(f), g, h);
1164 } else
1165 PUSHREF(zite_rec(f, g, LOW(h)));
1166 res = zdd_makenode(LEVEL(h), HIGH(h), READREF(1));
1167 POPREF(1);
1168 }
1169 } else
1170 if (LEVEL(g) == LEVEL(h)) {
1171 PUSHREF(zite_rec(f, LOW(g), LOW(h)));
1172 res = zdd_makenode(LEVEL(g), HIGH(h), READREF(1));
1173 POPREF(1);
1174 } else if (LEVEL(g) < LEVEL(h)) {
1175 PUSHREF(zite_rec(f, LOW(g), h));
1176 res = zdd_makenode(LEVEL(g), 0, READREF(1));
1177 POPREF(1);
1178 } else
1179 PUSHREF(zite_rec(f, g, LOW(h)));
1180 res = zdd_makenode(LEVEL(h), HIGH(h), READREF(1));
1181 POPREF(1);
1182 }
1183 }
1184
1185 entry.a = f;
1186 entry.b = g;
1187 entry.c = h;
1188 entry.res = res;
1189
1190 return res;
1191 }
1192
1193 int bdd_replace(int r, bddPair pair) {
1194 int res;
1195 int numReorder = 1;
1196
1197 CHECKa(r, bddfalse);
1198
1199 if (replacecache == null) replacecache = BddCacheI_init(cachesize);
1200 if (ZDD && applycache == null) applycache = BddCacheI_init(cachesize);
1201
1202 again : for (;;) {
1203 try {
1204 INITREF();
1205 replacepair = pair.result;
1206 replacelast = pair.last;
1207 replaceid = (pair.id << 2) | CACHEID_REPLACE;
1208 if (ZDD) applyop = bddop_or;
1209
1210 if (numReorder == 0) bdd_disable_reorder();
1211 res = replace_rec(r);
1212 if (numReorder == 0) bdd_enable_reorder();
1213 } catch (ReorderException x) {
1214 bdd_checkreorder();
1215 numReorder--;
1216 continue again;
1217 }
1218 break;
1219 }
1220
1221 checkresize();
1222 return res;
1223 }
1224
1225 int replace_rec(int r) {
1226 BddCacheDataI entry;
1227 int res;
1228
1229 if (ISCONST(r) || LEVEL(r) > replacelast)
1230 return r;
1231
1232 entry = BddCache_lookupI(replacecache, REPLACEHASH(r));
1233 if (entry.a == r && entry.c == replaceid) {
1234 if (CACHESTATS)
1235 cachestats.opHit++;
1236 return entry.res;
1237 }
1238 if (CACHESTATS)
1239 cachestats.opMiss++;
1240
1241 PUSHREF(replace_rec(LOW(r)));
1242 PUSHREF(replace_rec(HIGH(r)));
1243
1244 if (ZDD)
1245 res =
1246 zdd_correctify(
1247 LEVEL(replacepair[LEVEL(r)]),
1248 READREF(2),
1249 READREF(1));
1250 else
1251 res =
1252 bdd_correctify(
1253 LEVEL(replacepair[LEVEL(r)]),
1254 READREF(2),
1255 READREF(1));
1256 POPREF(2);
1257
1258 entry.a = r;
1259 entry.c = replaceid;
1260 entry.res = res;
1261
1262 return res;
1263 }
1264
1265 int bdd_correctify(int level, int l, int r) {
1266 int res;
1267
1268 if (level < LEVEL(l) && level < LEVEL(r))
1269 return bdd_makenode(level, l, r);
1270
1271 if (level == LEVEL(l) || level == LEVEL(r)) {
1272 bdd_error(BDD_REPLACE);
1273 return 0;
1274 }
1275
1276 if (LEVEL(l) == LEVEL(r)) {
1277 PUSHREF(bdd_correctify(level, LOW(l), LOW(r)));
1278 PUSHREF(bdd_correctify(level, HIGH(l), HIGH(r)));
1279 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1280 } else if (LEVEL(l) < LEVEL(r)) {
1281 PUSHREF(bdd_correctify(level, LOW(l), r));
1282 PUSHREF(bdd_correctify(level, HIGH(l), r));
1283 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1284 } else {
1285 PUSHREF(bdd_correctify(level, l, LOW(r)));
1286 PUSHREF(bdd_correctify(level, l, HIGH(r)));
1287 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
1288 }
1289 POPREF(2);
1290
1291 return res;
1292 }
1293
1294 int zdd_correctify(int level, int l, int r) {
1295 int res;
1296
1297
1298
1299 PUSHREF(zdd_makenode(level, 0, 1));
1300 PUSHREF(zdd_change(r, READREF(1)));
1301 res = zor_rec(READREF(1), l);
1302 POPREF(2);
1303
1304 return res;
1305 }
1306
1307
1308 int zdd_change(int r, int zvar) {
1309 int res;
1310
1311 if (ISZERO(r))
1312 return r;
1313 if (ISONE(r))
1314 return zvar;
1315
1316 if (LEVEL(r) > LEVEL(zvar)) {
1317 res = zdd_makenode(LEVEL(zvar), BDDZERO, r);
1318 } else if (LEVEL(r) == LEVEL(zvar)) {
1319 res = zdd_makenode(LEVEL(zvar), HIGH(r), LOW(r));
1320 } else {
1321 PUSHREF(zdd_change(LOW(r), zvar));
1322 PUSHREF(zdd_change(HIGH(r), zvar));
1323 res = zdd_makenode(LEVEL(r), READREF(2), READREF(1));
1324 POPREF(2);
1325 }
1326
1327 return res;
1328 }
1329
1330 int bdd_apply(int l, int r, int op) {
1331 int res;
1332 int numReorder = 1;
1333
1334 CHECKa(l, bddfalse);
1335 CHECKa(r, bddfalse);
1336
1337 if (op < 0 || op > bddop_invimp) {
1338 bdd_error(BDD_OP);
1339 return bddfalse;
1340 }
1341
1342 if (applycache == null) applycache = BddCacheI_init(cachesize);
1343
1344 again : for (;;) {
1345 try {
1346 INITREF();
1347 applyop = op;
1348
1349 if (numReorder == 0) bdd_disable_reorder();
1350 if (ZDD) {
1351 switch (op) {
1352 case bddop_and: res = zand_rec(l, r); break;
1353 case bddop_or: res = zor_rec(l, r); break;
1354 case bddop_diff: res = zdiff_rec(l, r); break;
1355 case bddop_imp:
1356 {
1357
1358 int a = bdd_addref(zdiff_rec(l, r));
1359 res = zdiff_rec(univ, a);
1360 bdd_delref(a);
1361 break;
1362 }
1363 case bddop_invimp:
1364 {
1365
1366 int a = bdd_addref(zdiff_rec(r, l));
1367 res = zdiff_rec(univ, a);
1368 bdd_delref(a);
1369 break;
1370 }
1371 case bddop_less:
1372 {
1373
1374 res = zdiff_rec(r, l);
1375 break;
1376 }
1377 case bddop_nand:
1378 {
1379
1380 int k = bdd_addref(zand_rec(l, r));
1381 res = zdiff_rec(univ, k);
1382 bdd_delref(k);
1383 break;
1384 }
1385 case bddop_nor:
1386 {
1387
1388 int k = bdd_addref(zor_rec(l, r));
1389 res = zdiff_rec(univ, k);
1390 bdd_delref(k);
1391 break;
1392 }
1393 case bddop_xor:
1394 {
1395
1396 int a = bdd_addref(zand_rec(l, r));
1397 int b = bdd_addref(zor_rec(l, r));
1398 res = zdiff_rec(b, a);
1399 bdd_delref(a); bdd_delref(b);
1400 break;
1401 }
1402 case bddop_biimp:
1403 {
1404
1405 int a = bdd_addref(zand_rec(l, r));
1406 int b = bdd_addref(zor_rec(l, r));
1407 int c = bdd_addref(zdiff_rec(b, a));
1408 bdd_delref(a); bdd_delref(b);
1409 res = zdiff_rec(univ, c);
1410 bdd_delref(c);
1411 break;
1412 }
1413 default:
1414
1415 throw new BDDException();
1416 }
1417 } else {
1418 switch (op) {
1419 case bddop_and: res = and_rec(l, r); break;
1420 case bddop_or: res = or_rec(l, r); break;
1421 default: res = apply_rec(l, r); break;
1422 }
1423 }
1424 if (numReorder == 0) bdd_enable_reorder();
1425 } catch (ReorderException x) {
1426 bdd_checkreorder();
1427 numReorder--;
1428 continue again;
1429 }
1430 break;
1431 }
1432
1433 checkresize();
1434 if (false) bdd_validate(res);
1435 return res;
1436 }
1437
1438 int apply_rec(int l, int r) {
1439 BddCacheDataI entry;
1440 int res;
1441
1442 if (VERIFY_ASSERTIONS) _assert(!ZDD);
1443 if (VERIFY_ASSERTIONS) _assert(applyop != bddop_and && applyop != bddop_or);
1444
1445 switch (applyop) {
1446 case bddop_xor :
1447 if (l == r)
1448 return 0;
1449 if (ISZERO(l))
1450 return r;
1451 if (ISZERO(r))
1452 return l;
1453 break;
1454 case bddop_nand :
1455 if (ISZERO(l) || ISZERO(r))
1456 return 1;
1457 break;
1458 case bddop_nor :
1459 if (ISONE(l) || ISONE(r))
1460 return 0;
1461 break;
1462 case bddop_imp :
1463 if (ISZERO(l))
1464 return 1;
1465 if (ISONE(l))
1466 return r;
1467 if (ISONE(r))
1468 return 1;
1469 break;
1470 }
1471
1472 if (ISCONST(l) && ISCONST(r))
1473 res = oprres[applyop][l << 1 | r];
1474 else {
1475 entry = BddCache_lookupI(applycache, APPLYHASH(l, r, applyop));
1476
1477 if (entry.a == l && entry.b == r && entry.c == applyop) {
1478 if (CACHESTATS)
1479 cachestats.opHit++;
1480 return entry.res;
1481 }
1482 if (CACHESTATS)
1483 cachestats.opMiss++;
1484
1485 if (LEVEL(l) == LEVEL(r)) {
1486 PUSHREF(apply_rec(LOW(l), LOW(r)));
1487 PUSHREF(apply_rec(HIGH(l), HIGH(r)));
1488 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1489 } else if (LEVEL(l) < LEVEL(r)) {
1490 PUSHREF(apply_rec(LOW(l), r));
1491 PUSHREF(apply_rec(HIGH(l), r));
1492 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1493 } else {
1494 PUSHREF(apply_rec(l, LOW(r)));
1495 PUSHREF(apply_rec(l, HIGH(r)));
1496 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
1497 }
1498
1499 POPREF(2);
1500
1501 entry.a = l;
1502 entry.b = r;
1503 entry.c = applyop;
1504 entry.res = res;
1505 }
1506
1507 return res;
1508 }
1509
1510 int and_rec(int l, int r) {
1511 BddCacheDataI entry;
1512 int res;
1513
1514 if (l == r)
1515 return l;
1516 if (ISZERO(l) || ISZERO(r))
1517 return 0;
1518 if (ISONE(l))
1519 return r;
1520 if (ISONE(r))
1521 return l;
1522
1523 entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and));
1524
1525 if (entry.a == l && entry.b == r && entry.c == bddop_and) {
1526 if (CACHESTATS)
1527 cachestats.opHit++;
1528 return entry.res;
1529 }
1530 if (CACHESTATS)
1531 cachestats.opMiss++;
1532
1533 if (LEVEL(l) == LEVEL(r)) {
1534 PUSHREF(and_rec(LOW(l), LOW(r)));
1535 PUSHREF(and_rec(HIGH(l), HIGH(r)));
1536 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1537 } else if (LEVEL(l) < LEVEL(r)) {
1538 PUSHREF(and_rec(LOW(l), r));
1539 PUSHREF(and_rec(HIGH(l), r));
1540 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1541 } else {
1542 PUSHREF(and_rec(l, LOW(r)));
1543 PUSHREF(and_rec(l, HIGH(r)));
1544 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
1545 }
1546
1547 POPREF(2);
1548
1549 entry.a = l;
1550 entry.b = r;
1551 entry.c = bddop_and;
1552 entry.res = res;
1553
1554 return res;
1555 }
1556
1557 int zand_rec(int l, int r) {
1558 BddCacheDataI entry;
1559 int res;
1560
1561 if (l == r)
1562 return l;
1563 if (ISZERO(l) || ISZERO(r))
1564 return 0;
1565 if (LEVEL(l) < LEVEL(r))
1566 return zand_rec(LOW(l), r);
1567 else if (LEVEL(l) > LEVEL(r))
1568 return zand_rec(l, LOW(r));
1569 if (VERIFY_ASSERTIONS) _assert(!ISCONST(l) && !ISCONST(r));
1570
1571 entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_and));
1572
1573 if (entry.a == l && entry.b == r && entry.c == bddop_and) {
1574 if (CACHESTATS)
1575 cachestats.opHit++;
1576 return entry.res;
1577 }
1578 if (CACHESTATS)
1579 cachestats.opMiss++;
1580
1581 PUSHREF(zand_rec(LOW(l), LOW(r)));
1582 PUSHREF(zand_rec(HIGH(l), HIGH(r)));
1583 res = zdd_makenode(LEVEL(l), READREF(2), READREF(1));
1584
1585 POPREF(2);
1586
1587 entry.a = l;
1588 entry.b = r;
1589 entry.c = bddop_and;
1590 entry.res = res;
1591
1592 return res;
1593 }
1594
1595 int zrelprod_rec(int l, int r, int lev) {
1596 BddCacheDataI entry;
1597 int res;
1598
1599 if (l == r)
1600 return zquant_rec(l, lev);
1601 if (ISZERO(l) || ISZERO(r))
1602 return 0;
1603
1604 int LEVEL_l = LEVEL(l);
1605 int LEVEL_r = LEVEL(r);
1606
1607 for (;;) {
1608 if (lev > quantlast) {
1609 applyop = bddop_and;
1610 res = zand_rec(l, r);
1611 applyop = bddop_or;
1612 return res;
1613 }
1614 if (lev >= LEVEL_l || lev >= LEVEL_r)
1615 break;
1616 if (INVARSET(lev)) {
1617 res = zrelprod_rec(l, r, lev+1);
1618 PUSHREF(res);
1619 res = zdd_makenode(lev, res, res);
1620 POPREF(1);
1621 return res;
1622 }
1623 ++lev;
1624 }
1625
1626 entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, bddop_and));
1627 if (entry.a == l && entry.b == r && entry.c == appexid) {
1628 if (CACHESTATS)
1629 cachestats.opHit++;
1630 return entry.res;
1631 }
1632 if (CACHESTATS)
1633 cachestats.opMiss++;
1634
1635 if (LEVEL_l == LEVEL_r) {
1636 if (VERIFY_ASSERTIONS) _assert(LEVEL_l == lev);
1637 PUSHREF(zrelprod_rec(LOW(l), LOW(r), lev+1));
1638 PUSHREF(zrelprod_rec(HIGH(l), HIGH(r), lev+1));
1639 if (INVARSET(lev)) {
1640 res = zor_rec(READREF(2), READREF(1));
1641 POPREF(2);
1642 PUSHREF(res);
1643 res = zdd_makenode(lev, res, res);
1644 POPREF(1);
1645 } else {
1646 res = zdd_makenode(lev, READREF(2), READREF(1));
1647 POPREF(2);
1648 }
1649 } else {
1650 if (LEVEL_l < LEVEL_r) {
1651 if (VERIFY_ASSERTIONS) _assert(LEVEL_l == lev);
1652 res = zrelprod_rec(LOW(l), r, lev+1);
1653 } else {
1654 if (VERIFY_ASSERTIONS) _assert(LEVEL_r == lev);
1655 res = zrelprod_rec(l, LOW(r), lev+1);
1656 }
1657 if (INVARSET(lev)) {
1658 PUSHREF(res);
1659 res = zdd_makenode(lev, res, res);
1660 POPREF(1);
1661 }
1662 }
1663 entry.a = l;
1664 entry.b = r;
1665 entry.c = appexid;
1666 entry.res = res;
1667
1668 return res;
1669 }
1670
1671 int or_rec(int l, int r) {
1672 BddCacheDataI entry;
1673 int res;
1674
1675 if (l == r)
1676 return l;
1677 if (ISONE(l) || ISONE(r))
1678 return 1;
1679 if (ISZERO(l))
1680 return r;
1681 if (ISZERO(r))
1682 return l;
1683 entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_or));
1684
1685 if (entry.a == l && entry.b == r && entry.c == bddop_or) {
1686 if (CACHESTATS)
1687 cachestats.opHit++;
1688 return entry.res;
1689 }
1690 if (CACHESTATS)
1691 cachestats.opMiss++;
1692
1693 if (LEVEL(l) == LEVEL(r)) {
1694 PUSHREF(or_rec(LOW(l), LOW(r)));
1695 PUSHREF(or_rec(HIGH(l), HIGH(r)));
1696 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1697 } else if (LEVEL(l) < LEVEL(r)) {
1698 PUSHREF(or_rec(LOW(l), r));
1699 PUSHREF(or_rec(HIGH(l), r));
1700 res = bdd_makenode(LEVEL(l), READREF(2), READREF(1));
1701 } else {
1702 PUSHREF(or_rec(l, LOW(r)));
1703 PUSHREF(or_rec(l, HIGH(r)));
1704 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
1705 }
1706
1707 POPREF(2);
1708
1709 entry.a = l;
1710 entry.b = r;
1711 entry.c = bddop_or;
1712 entry.res = res;
1713
1714 return res;
1715 }
1716
1717 int zor_rec(int l, int r) {
1718 BddCacheDataI entry;
1719 int res;
1720
1721 if (l == r)
1722 return l;
1723
1724
1725 if (ISZERO(l))
1726 return r;
1727 if (ISZERO(r))
1728 return l;
1729 entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_or));
1730
1731 if (entry.a == l && entry.b == r && entry.c == bddop_or) {
1732 if (CACHESTATS)
1733 cachestats.opHit++;
1734 return entry.res;
1735 }
1736 if (CACHESTATS)
1737 cachestats.opMiss++;
1738
1739 if (LEVEL(l) == LEVEL(r)) {
1740 PUSHREF(zor_rec(LOW(l), LOW(r)));
1741 PUSHREF(zor_rec(HIGH(l), HIGH(r)));
1742 res = zdd_makenode(LEVEL(l), READREF(2), READREF(1));
1743 POPREF(2);
1744 } else {
1745 if (LEVEL(l) < LEVEL(r)) {
1746 PUSHREF(zor_rec(LOW(l), r));
1747 res = zdd_makenode(LEVEL(l), READREF(1), HIGH(l));
1748 } else {
1749 PUSHREF(zor_rec(l, LOW(r)));
1750 res = zdd_makenode(LEVEL(r), READREF(1), HIGH(r));
1751 }
1752 POPREF(1);
1753 }
1754
1755 entry.a = l;
1756 entry.b = r;
1757 entry.c = bddop_or;
1758 entry.res = res;
1759
1760 return res;
1761 }
1762
1763 int zdiff_rec(int l, int r) {
1764 BddCacheDataI entry;
1765 int res;
1766
1767 if (ISZERO(l)
1768 return 0;
1769 if (ISZERO(r))
1770 return l;
1771 if (LEVEL(l) > LEVEL(r))
1772 return zdiff_rec(l, LOW(r));
1773
1774 entry = BddCache_lookupI(applycache, APPLYHASH(l, r, bddop_diff));
1775
1776 if (entry.a == l && entry.b == r && entry.c == bddop_diff) {
1777 if (CACHESTATS)
1778 cachestats.opHit++;
1779 return entry.res;
1780 }
1781 if (CACHESTATS)
1782 cachestats.opMiss++;
1783
1784 if (LEVEL(l) == LEVEL(r)) {
1785 PUSHREF(zdiff_rec(LOW(l), LOW(r)));
1786 PUSHREF(zdiff_rec(HIGH(l), HIGH(r)));
1787 res = zdd_makenode(LEVEL(l), READREF(2), READREF(1));
1788 POPREF(2);
1789 } else {
1790 PUSHREF(zdiff_rec(LOW(l), r));
1791 res = zdd_makenode(LEVEL(l), READREF(1), HIGH(l));
1792 POPREF(1);
1793 }
1794
1795 entry.a = l;
1796 entry.b = r;
1797 entry.c = bddop_diff;
1798 entry.res = res;
1799
1800 return res;
1801 }
1802
1803 int relprod_rec(int l, int r) {
1804 BddCacheDataI entry;
1805 int res;
1806
1807 if (VERIFY_ASSERTIONS) _assert(!ZDD);
1808
1809 if (l == 0 || r == 0)
1810 return 0;
1811 if (l == r)
1812 return quant_rec(l);
1813 if (l == 1)
1814 return quant_rec(r);
1815 if (r == 1)
1816 return quant_rec(l);
1817
1818 int LEVEL_l = LEVEL(l);
1819 int LEVEL_r = LEVEL(r);
1820 if (LEVEL_l > quantlast && LEVEL_r > quantlast) {
1821 applyop = bddop_and;
1822 res = and_rec(l, r);
1823 applyop = bddop_or;
1824 } else {
1825 entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, bddop_and));
1826 if (entry.a == l && entry.b == r && entry.c == appexid) {
1827 if (CACHESTATS)
1828 cachestats.opHit++;
1829 return entry.res;
1830 }
1831 if (CACHESTATS)
1832 cachestats.opMiss++;
1833
1834 if (LEVEL_l == LEVEL_r) {
1835 PUSHREF(relprod_rec(LOW(l), LOW(r)));
1836 PUSHREF(relprod_rec(HIGH(l), HIGH(r)));
1837 if (INVARSET(LEVEL_l))
1838 res = or_rec(READREF(2), READREF(1));
1839 else
1840 res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
1841 } else if (LEVEL_l < LEVEL_r) {
1842 PUSHREF(relprod_rec(LOW(l), r));
1843 PUSHREF(relprod_rec(HIGH(l), r));
1844 if (INVARSET(LEVEL_l))
1845 res = or_rec(READREF(2), READREF(1));
1846 else
1847 res = bdd_makenode(LEVEL_l, READREF(2), READREF(1));
1848 } else {
1849 PUSHREF(relprod_rec(l, LOW(r)));
1850 PUSHREF(relprod_rec(l, HIGH(r)));
1851 if (INVARSET(LEVEL_r))
1852 res = or_rec(READREF(2), READREF(1));
1853 else
1854 res = bdd_makenode(LEVEL_r, READREF(2), READREF(1));
1855 }
1856
1857 POPREF(2);
1858
1859 entry.a = l;
1860 entry.b = r;
1861 entry.c = appexid;
1862 entry.res = res;
1863 }
1864
1865 return res;
1866 }
1867
1868 int bdd_relprod(int a, int b, int var) {
1869 return bdd_appex(a, b, bddop_and, var);
1870 }
1871
1872 int bdd_appex(int l, int r, int opr, int var) {
1873 int res;
1874 int numReorder = 1;
1875
1876 CHECKa(l, bddfalse);
1877 CHECKa(r, bddfalse);
1878 CHECKa(var, bddfalse);
1879
1880 if (opr < 0 || opr > bddop_invimp) {
1881 bdd_error(BDD_OP);
1882 return bddfalse;
1883 }
1884
1885 if (var < 2)
1886 return bdd_apply(l, r, opr);
1887
1888 if (applycache == null) applycache = BddCacheI_init(cachesize);
1889 if (appexcache == null) appexcache = BddCacheI_init(cachesize);
1890 if (quantcache == null) quantcache = BddCacheI_init(cachesize);
1891
1892 again : for (;;) {
1893 if (varset2vartable(var) < 0)
1894 return bddfalse;
1895 try {
1896 INITREF();
1897
1898 applyop = bddop_or;
1899 appexop = opr;
1900 appexid = (var << 5) | (appexop << 1);
1901 quantid = (appexid << 3) | CACHEID_APPEX;
1902
1903 if (numReorder == 0)
1904 bdd_disable_reorder();
1905 if (opr == bddop_and)
1906 res = ZDD ? zrelprod_rec(l, r, 0) : relprod_rec(l, r);
1907 else
1908 res = appquant_rec(l, r);
1909
1910 if (numReorder == 0)
1911 bdd_enable_reorder();
1912 } catch (ReorderException x) {
1913 bdd_checkreorder();
1914
1915 numReorder--;
1916 continue again;
1917 }
1918 break;
1919 }
1920
1921 checkresize();
1922 return res;
1923 }
1924
1925 int varset2vartable(int r) {
1926 int n;
1927
1928 if (r < 2)
1929 return bdd_error(BDD_VARSET);
1930
1931 quantvarsetID++;
1932
1933 if (quantvarsetID == INT_MAX) {
1934 for (int i = 0; i < bddvarnum; ++i)
1935 quantvarset[i] = 0;
1936 quantvarsetID = 1;
1937 }
1938
1939 quantlast = -1;
1940 for (n = r; n > 1; n = HIGH(n)) {
1941 quantvarset[LEVEL(n)] = quantvarsetID;
1942 if (VERIFY_ASSERTIONS) _assert(quantlast < LEVEL(n));
1943 quantlast = LEVEL(n);
1944 }
1945
1946 return 0;
1947 }
1948
1949 static final int INT_MAX = Integer.MAX_VALUE;
1950
1951 int varset2svartable(int r) {
1952 int n;
1953
1954 if (r < 2)
1955 return bdd_error(BDD_VARSET);
1956
1957 quantvarsetID++;
1958
1959 if (quantvarsetID == INT_MAX / 2) {
1960 for (int i = 0; i < bddvarnum; ++i)
1961 quantvarset[i] = 0;
1962 quantvarsetID = 1;
1963 }
1964
1965 quantlast = 0;
1966 for (n = r; !ISCONST(n);) {
1967 if (ISZERO(LOW(n))) {
1968 quantvarset[LEVEL(n)] = quantvarsetID;
1969 n = HIGH(n);
1970 } else {
1971 quantvarset[LEVEL(n)] = -quantvarsetID;
1972 n = LOW(n);
1973 }
1974 if (VERIFY_ASSERTIONS) _assert(quantlast < LEVEL(n));
1975 quantlast = LEVEL(n);
1976 }
1977
1978 return 0;
1979 }
1980
1981 int appquant_rec(int l, int r) {
1982 BddCacheDataI entry;
1983 int res;
1984
1985 if (VERIFY_ASSERTIONS) _assert(appexop != bddop_and);
1986
1987 switch (appexop) {
1988 case bddop_or :
1989 if (l == 1 || r == 1)
1990 return 1;
1991 if (l == r)
1992 return quant_rec(l);
1993 if (l == 0)
1994 return quant_rec(r);
1995 if (r == 0)
1996 return quant_rec(l);
1997 break;
1998 case bddop_xor :
1999 if (l == r)
2000 return 0;
2001 if (l == 0)
2002 return quant_rec(r);
2003 if (r == 0)
2004 return quant_rec(l);
2005 break;
2006 case bddop_nand :
2007 if (l == 0 || r == 0)
2008 return 1;
2009 break;
2010 case bddop_nor :
2011 if (l == 1 || r == 1)
2012 return 0;
2013 break;
2014 }
2015
2016 if (ISCONST(l) && ISCONST(r))
2017 res = oprres[appexop][(l << 1) | r];
2018 else if (LEVEL(l) > quantlast && LEVEL(r) > quantlast) {
2019 int oldop = applyop;
2020 applyop = appexop;
2021 switch (applyop) {
2022 case bddop_and: res = and_rec(l, r); break;
2023 case bddop_or: res = or_rec(l, r); break;
2024 default: res = apply_rec(l, r); break;
2025 }
2026 applyop = oldop;
2027 } else {
2028 entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, appexop));
2029 if (entry.a == l && entry.b == r && entry.c == appexid) {
2030 if (CACHESTATS)
2031 cachestats.opHit++;
2032 return entry.res;
2033 }
2034 if (CACHESTATS)
2035 cachestats.opMiss++;
2036
2037 int lev;
2038 if (LEVEL(l) == LEVEL(r)) {
2039 PUSHREF(appquant_rec(LOW(l), LOW(r)));
2040 PUSHREF(appquant_rec(HIGH(l), HIGH(r)));
2041 lev = LEVEL(l);
2042 } else if (LEVEL(l) < LEVEL(r)) {
2043 PUSHREF(appquant_rec(LOW(l), r));
2044 PUSHREF(appquant_rec(HIGH(l), r));
2045 lev = LEVEL(l);
2046 } else {
2047 PUSHREF(appquant_rec(l, LOW(r)));
2048 PUSHREF(appquant_rec(l, HIGH(r)));
2049 lev = LEVEL(r);
2050 }
2051 if (INVARSET(lev)) {
2052 int r2 = READREF(2), r1 = READREF(1);
2053 switch (applyop) {
2054 case bddop_and: res = and_rec(r2, r1); break;
2055 case bddop_or: res = or_rec(r2, r1); break;
2056 default: res = apply_rec(r2, r1); break;
2057 }
2058 } else {
2059 res = bdd_makenode(lev, READREF(2), READREF(1));
2060 }
2061
2062 POPREF(2);
2063
2064 entry.a = l;
2065 entry.b = r;
2066 entry.c = appexid;
2067 entry.res = res;
2068 }
2069
2070 return res;
2071 }
2072
2073 int appuni_rec(int l, int r, int var) {
2074 BddCacheDataI entry;
2075 int res;
2076
2077 int LEVEL_l, LEVEL_r, LEVEL_var;
2078 LEVEL_l = LEVEL(l);
2079 LEVEL_r = LEVEL(r);
2080 LEVEL_var = LEVEL(var);
2081
2082 if (LEVEL_l > LEVEL_var && LEVEL_r > LEVEL_var) {
2083
2084 return BDDZERO;
2085 }
2086
2087 if (ISCONST(l) && ISCONST(r))
2088 res = oprres[appexop][(l << 1) | r];
2089 else if (ISCONST(var)) {
2090 int oldop = applyop;
2091 applyop = appexop;
2092 switch (applyop) {
2093 case bddop_and: res = and_rec(l, r); break;
2094 case bddop_or: res = or_rec(l, r); break;
2095 default: res = apply_rec(l, r); break;
2096 }
2097 applyop = oldop;
2098 } else {
2099 entry = BddCache_lookupI(appexcache, APPEXHASH(l, r, appexop));
2100 if (entry.a == l && entry.b == r && entry.c == appexid) {
2101 if (CACHESTATS)
2102 cachestats.opHit++;
2103 return entry.res;
2104 }
2105 if (CACHESTATS)
2106 cachestats.opMiss++;
2107
2108 int lev;
2109 if (LEVEL_l == LEVEL_r) {
2110 if (LEVEL_l == LEVEL_var) {
2111 lev = -1;
2112 var = HIGH(var);
2113 } else {
2114 lev = LEVEL_l;
2115 }
2116 PUSHREF(appuni_rec(LOW(l), LOW(r), var));
2117 PUSHREF(appuni_rec(HIGH(l), HIGH(r), var));
2118 lev = LEVEL_l;
2119 } else if (LEVEL_l < LEVEL_r) {
2120 if (LEVEL_l == LEVEL_var) {
2121 lev = -1;
2122 var = HIGH(var);
2123 } else {
2124 lev = LEVEL_l;
2125 }
2126 PUSHREF(appuni_rec(LOW(l), r, var));
2127 PUSHREF(appuni_rec(HIGH(l), r, var));
2128 } else {
2129 if (LEVEL_r == LEVEL_var) {
2130 lev = -1;
2131 var = HIGH(var);
2132 } else {
2133 lev = LEVEL_r;
2134 }
2135 PUSHREF(appuni_rec(l, LOW(r), var));
2136 PUSHREF(appuni_rec(l, HIGH(r), var));
2137 }
2138 if (lev == -1) {
2139 int r2 = READREF(2), r1 = READREF(1);
2140 switch (applyop) {
2141 case bddop_and: res = and_rec(r2, r1); break;
2142 case bddop_or: res = or_rec(r2, r1); break;
2143 default: res = apply_rec(r2, r1); break;
2144 }
2145 } else {
2146 res = bdd_makenode(lev, READREF(2), READREF(1));
2147 }
2148
2149 POPREF(2);
2150
2151 entry.a = l;
2152 entry.b = r;
2153 entry.c = appexid;
2154 entry.res = res;
2155 }
2156
2157 return res;
2158 }
2159
2160 int unique_rec(int r, int q) {
2161 BddCacheDataI entry;
2162 int res;
2163 int LEVEL_r, LEVEL_q;
2164
2165 LEVEL_r = LEVEL(r);
2166 LEVEL_q = LEVEL(q);
2167 if (LEVEL_r > LEVEL_q) {
2168
2169 return BDDZERO;
2170 }
2171
2172 if (r < 2 || q < 2)
2173 return r;
2174
2175 entry = BddCache_lookupI(quantcache, QUANTHASH(r));
2176 if (entry.a == r && entry.c == quantid) {
2177 if (CACHESTATS)
2178 cachestats.opHit++;
2179 return entry.res;
2180 }
2181 if (CACHESTATS)
2182 cachestats.opMiss++;
2183
2184 if (LEVEL_r == LEVEL_q) {
2185 PUSHREF(unique_rec(LOW(r), HIGH(q)));
2186 PUSHREF(unique_rec(HIGH(r), HIGH(q)));
2187 res = apply_rec(READREF(2), READREF(1));
2188 } else {
2189 PUSHREF(unique_rec(LOW(r), q));
2190 PUSHREF(unique_rec(HIGH(r), q));
2191 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
2192 }
2193
2194 POPREF(2);
2195
2196 entry.a = r;
2197 entry.c = quantid;
2198 entry.res = res;
2199
2200 return res;
2201 }
2202
2203 int quant_rec(int r) {
2204 BddCacheDataI entry;
2205 int res;
2206
2207 if (r < 2 || LEVEL(r) > quantlast)
2208 return r;
2209
2210 entry = BddCache_lookupI(quantcache, QUANTHASH(r));
2211 if (entry.a == r && entry.c == quantid) {
2212 if (CACHESTATS)
2213 cachestats.opHit++;
2214 return entry.res;
2215 }
2216 if (CACHESTATS)
2217 cachestats.opMiss++;
2218
2219 PUSHREF(quant_rec(LOW(r)));
2220 PUSHREF(quant_rec(HIGH(r)));
2221
2222 if (INVARSET(LEVEL(r))) {
2223 int r2 = READREF(2), r1 = READREF(1);
2224 switch (applyop) {
2225 case bddop_and: res = and_rec(r2, r1); break;
2226 case bddop_or: res = or_rec(r2, r1); break;
2227 default: res = apply_rec(r2, r1); break;
2228 }
2229 } else {
2230 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
2231 }
2232
2233 POPREF(2);
2234
2235 entry.a = r;
2236 entry.c = quantid;
2237 entry.res = res;
2238
2239 return res;
2240 }
2241
2242 int zquant_rec(int r, int lev) {
2243 BddCacheDataI entry;
2244 int res;
2245
2246 for (;;) {
2247 if (lev > quantlast)
2248 return r;
2249 if (lev == LEVEL(r))
2250 break;
2251 if (INVARSET(lev)) {
2252 switch (applyop) {
2253 case bddop_and: return 0;
2254 case bddop_or:
2255 PUSHREF(zquant_rec(r, lev+1));
2256 res = zdd_makenode(lev, READREF(1), READREF(1));
2257 POPREF(1);
2258 return res;
2259 default: throw new BDDException();
2260 }
2261 }
2262 lev++;
2263 }
2264
2265 if (r < 2)
2266 return r;
2267
2268 entry = BddCache_lookupI(quantcache, QUANTHASH(r));
2269 if (entry.a == r && entry.c == quantid) {
2270 if (CACHESTATS)
2271 cachestats.opHit++;
2272 return entry.res;
2273 }
2274 if (CACHESTATS)
2275 cachestats.opMiss++;
2276
2277 int nlev = LEVEL(r) + 1;
2278 PUSHREF(zquant_rec(LOW(r), nlev));
2279 PUSHREF(zquant_rec(HIGH(r), nlev));
2280
2281 if (INVARSET(LEVEL(r))) {
2282 int r2 = READREF(2), r1 = READREF(1);
2283 switch (applyop) {
2284 case bddop_and: res = zand_rec(r2, r1); break;
2285 case bddop_or: res = zor_rec(r2, r1); break;
2286 default: throw new BDDException();
2287 }
2288 POPREF(2);
2289 PUSHREF(res);
2290 res = zdd_makenode(LEVEL(r), READREF(1), READREF(1));
2291 POPREF(1);
2292 } else {
2293 res = zdd_makenode(LEVEL(r), READREF(2), READREF(1));
2294 POPREF(2);
2295 }
2296
2297 entry.a = r;
2298 entry.c = quantid;
2299 entry.res = res;
2300
2301 return res;
2302 }
2303
2304 int bdd_constrain(int f, int c) {
2305 int res;
2306 int numReorder = 1;
2307
2308 CHECKa(f, bddfalse);
2309 CHECKa(c, bddfalse);
2310
2311 if (misccache == null) misccache = BddCacheI_init(cachesize);
2312
2313 again : for (;;) {
2314 try {
2315 INITREF();
2316 miscid = CACHEID_CONSTRAIN;
2317
2318 if (numReorder == 0)
2319 bdd_disable_reorder();
2320 res = constrain_rec(f, c);
2321 if (numReorder == 0)
2322 bdd_enable_reorder();
2323 } catch (ReorderException x) {
2324 bdd_checkreorder();
2325
2326 numReorder--;
2327 continue again;
2328 }
2329 break;
2330 }
2331
2332 checkresize();
2333 return res;
2334 }
2335
2336 int constrain_rec(int f, int c) {
2337 BddCacheDataI entry;
2338 int res;
2339
2340 if (ISONE(c))
2341 return f;
2342 if (ISCONST(f))
2343 return f;
2344 if (c == f)
2345 return BDDONE;
2346 if (ISZERO(c))
2347 return BDDZERO;
2348
2349 entry = BddCache_lookupI(misccache, CONSTRAINHASH(f, c));
2350 if (entry.a == f && entry.b == c && entry.c == miscid) {
2351 if (CACHESTATS)
2352 cachestats.opHit++;
2353 return entry.res;
2354 }
2355 if (CACHESTATS)
2356 cachestats.opMiss++;
2357
2358 if (LEVEL(f) == LEVEL(c)) {
2359 if (ISZERO(LOW(c)))
2360 res = constrain_rec(HIGH(f), HIGH(c));
2361 else if (ISZERO(HIGH(c)))
2362 res = constrain_rec(LOW(f), LOW(c));
2363 else {
2364 PUSHREF(constrain_rec(LOW(f), LOW(c)));
2365 PUSHREF(constrain_rec(HIGH(f), HIGH(c)));
2366 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
2367 POPREF(2);
2368 }
2369 } else if (LEVEL(f) < LEVEL(c)) {
2370 PUSHREF(constrain_rec(LOW(f), c));
2371 PUSHREF(constrain_rec(HIGH(f), c));
2372 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
2373 POPREF(2);
2374 } else {
2375 if (ISZERO(LOW(c)))
2376 res = constrain_rec(f, HIGH(c));
2377 else if (ISZERO(HIGH(c)))
2378 res = constrain_rec(f, LOW(c));
2379 else {
2380 PUSHREF(constrain_rec(f, LOW(c)));
2381 PUSHREF(constrain_rec(f, HIGH(c)));
2382 res = bdd_makenode(LEVEL(c), READREF(2), READREF(1));
2383 POPREF(2);
2384 }
2385 }
2386
2387 entry.a = f;
2388 entry.b = c;
2389 entry.c = miscid;
2390 entry.res = res;
2391
2392 return res;
2393 }
2394
2395 int bdd_compose(int f, int g, int var) {
2396 int res;
2397 int numReorder = 1;
2398
2399 CHECKa(f, bddfalse);
2400 CHECKa(g, bddfalse);
2401 if (var < 0 || var >= bddvarnum) {
2402 bdd_error(BDD_VAR);
2403 return bddfalse;
2404 }
2405
2406 if (applycache == null) applycache = BddCacheI_init(cachesize);
2407 if (itecache == null) itecache = BddCacheI_init(cachesize);
2408
2409 again : for (;;) {
2410 try {
2411 INITREF();
2412 composelevel = bddvar2level[var];
2413 replaceid = (composelevel << 2) | CACHEID_COMPOSE;
2414
2415 if (numReorder == 0)
2416 bdd_disable_reorder();
2417 res = compose_rec(f, g);
2418 if (numReorder == 0)
2419 bdd_enable_reorder();
2420 } catch (ReorderException x) {
2421 bdd_checkreorder();
2422
2423 numReorder--;
2424 continue again;
2425 }
2426 break;
2427 }
2428
2429 checkresize();
2430 return res;
2431 }
2432
2433 int compose_rec(int f, int g) {
2434 BddCacheDataI entry;
2435 int res;
2436
2437 if (LEVEL(f) > composelevel)
2438 return f;
2439
2440 entry = BddCache_lookupI(replacecache, COMPOSEHASH(f, g));
2441 if (entry.a == f && entry.b == g && entry.c == replaceid) {
2442 if (CACHESTATS)
2443 cachestats.opHit++;
2444 return entry.res;
2445 }
2446 if (CACHESTATS)
2447 cachestats.opMiss++;
2448
2449 if (LEVEL(f) < composelevel) {
2450 if (LEVEL(f) == LEVEL(g)) {
2451 PUSHREF(compose_rec(LOW(f), LOW(g)));
2452 PUSHREF(compose_rec(HIGH(f), HIGH(g)));
2453 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
2454 } else if (LEVEL(f) < LEVEL(g)) {
2455 PUSHREF(compose_rec(LOW(f), g));
2456 PUSHREF(compose_rec(HIGH(f), g));
2457 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
2458 } else {
2459 PUSHREF(compose_rec(f, LOW(g)));
2460 PUSHREF(compose_rec(f, HIGH(g)));
2461 res = bdd_makenode(LEVEL(g), READREF(2), READREF(1));
2462 }
2463 POPREF(2);
2464 } else
2465
2466 res = ite_rec(g, HIGH(f), LOW(f));
2467 }
2468
2469 entry.a = f;
2470 entry.b = g;
2471 entry.c = replaceid;
2472 entry.res = res;
2473
2474 return res;
2475 }
2476
2477 int bdd_veccompose(int f, bddPair pair) {
2478 int res;
2479 int numReorder = 1;
2480
2481 CHECKa(f, bddfalse);
2482
2483 if (applycache == null) applycache = BddCacheI_init(cachesize);
2484 if (itecache == null) itecache = BddCacheI_init(cachesize);
2485 if (replacecache == null) replacecache = BddCacheI_init(cachesize);
2486
2487 again : for (;;) {
2488 try {
2489 INITREF();
2490 replacepair = pair.result;
2491 replaceid = (pair.id << 2) | CACHEID_VECCOMPOSE;
2492 replacelast = pair.last;
2493
2494 if (numReorder == 0)
2495 bdd_disable_reorder();
2496 res = veccompose_rec(f);
2497 if (numReorder == 0)
2498 bdd_enable_reorder();
2499 } catch (ReorderException x) {
2500 bdd_checkreorder();
2501
2502 numReorder--;
2503 continue again;
2504 }
2505 break;
2506 }
2507
2508 checkresize();
2509 return res;
2510 }
2511
2512 int veccompose_rec(int f) {
2513 BddCacheDataI entry;
2514 int res;
2515
2516 if (LEVEL(f) > replacelast)
2517 return f;
2518
2519 entry = BddCache_lookupI(replacecache, VECCOMPOSEHASH(f));
2520 if (entry.a == f && entry.c == replaceid) {
2521 if (CACHESTATS)
2522 cachestats.opHit++;
2523 return entry.res;
2524 }
2525 if (CACHESTATS)
2526 cachestats.opMiss++;
2527
2528 PUSHREF(veccompose_rec(LOW(f)));
2529 PUSHREF(veccompose_rec(HIGH(f)));
2530 res = ite_rec(replacepair[LEVEL(f)], READREF(1), READREF(2));
2531 POPREF(2);
2532
2533 entry.a = f;
2534 entry.c = replaceid;
2535 entry.res = res;
2536
2537 return res;
2538 }
2539
2540 int bdd_exist(int r, int var) {
2541 int res;
2542 int numReorder = 1;
2543
2544 CHECKa(r, bddfalse);
2545 CHECKa(var, bddfalse);
2546
2547 if (var < 2)
2548 return r;
2549
2550 if (applycache == null) applycache = BddCacheI_init(cachesize);
2551 if (quantcache == null) quantcache = BddCacheI_init(cachesize);
2552
2553 again : for (;;) {
2554 if (varset2vartable(var) < 0)
2555 return bddfalse;
2556 try {
2557 INITREF();
2558
2559 quantid = (var << 3) | CACHEID_EXIST;
2560 applyop = bddop_or;
2561
2562 if (numReorder == 0)
2563 bdd_disable_reorder();
2564 res = ZDD?zquant_rec(r, 0):quant_rec(r);
2565 if (numReorder == 0)
2566 bdd_enable_reorder();
2567 } catch (ReorderException x) {
2568 bdd_checkreorder();
2569
2570 numReorder--;
2571 continue again;
2572 }
2573 break;
2574 }
2575
2576 checkresize();
2577 if (false) bdd_validate(res);
2578 return res;
2579 }
2580
2581 int bdd_forall(int r, int var) {
2582 int res;
2583 int numReorder = 1;
2584
2585 CHECKa(r, bddfalse);
2586 CHECKa(var, bddfalse);
2587
2588 if (var < 2)
2589 return r;
2590
2591 if (applycache == null) applycache = BddCacheI_init(cachesize);
2592 if (quantcache == null) quantcache = BddCacheI_init(cachesize);
2593
2594 again : for (;;) {
2595 if (varset2vartable(var) < 0)
2596 return bddfalse;
2597 try {
2598 INITREF();
2599 quantid = (var << 3) | CACHEID_FORALL;
2600 applyop = bddop_and;
2601
2602 if (numReorder == 0)
2603 bdd_disable_reorder();
2604 res = ZDD?zquant_rec(r, 0):quant_rec(r);
2605 if (numReorder == 0)
2606 bdd_enable_reorder();
2607 } catch (ReorderException x) {
2608 bdd_checkreorder();
2609
2610 numReorder--;
2611 continue again;
2612 }
2613 break;
2614 }
2615
2616 checkresize();
2617 return res;
2618 }
2619
2620 int bdd_unique(int r, int var) {
2621 int res;
2622 int numReorder = 1;
2623
2624 CHECKa(r, bddfalse);
2625 CHECKa(var, bddfalse);
2626
2627 if (var < 2)
2628 return r;
2629
2630 if (applycache == null) applycache = BddCacheI_init(cachesize);
2631 if (quantcache == null) quantcache = BddCacheI_init(cachesize);
2632
2633 again : for (;;) {
2634 try {
2635 INITREF();
2636 quantid = (var << 3) | CACHEID_UNIQUE;
2637 applyop = bddop_xor;
2638
2639 if (numReorder == 0)
2640 bdd_disable_reorder();
2641 res = unique_rec(r, var);
2642 if (numReorder == 0)
2643 bdd_enable_reorder();
2644 } catch (ReorderException x) {
2645 bdd_checkreorder();
2646
2647 numReorder--;
2648 continue again;
2649 }
2650 break;
2651 }
2652
2653 checkresize();
2654 return res;
2655 }
2656
2657 int bdd_restrict(int r, int var) {
2658 int res;
2659 int numReorder = 1;
2660
2661 CHECKa(r, bddfalse);
2662 CHECKa(var, bddfalse);
2663
2664 if (var < 2)
2665 return r;
2666
2667 if (misccache == null) misccache = BddCacheI_init(cachesize);
2668
2669 again : for (;;) {
2670 if (varset2svartable(var) < 0)
2671 return bddfalse;
2672 try {
2673 INITREF();
2674 miscid = (var << 3) | CACHEID_RESTRICT;
2675
2676 if (numReorder == 0)
2677 bdd_disable_reorder();
2678 res = restrict_rec(r);
2679 if (numReorder == 0)
2680 bdd_enable_reorder();
2681 } catch (ReorderException x) {
2682 bdd_checkreorder();
2683
2684 numReorder--;
2685 continue again;
2686 }
2687 break;
2688 }
2689
2690 checkresize();
2691 return res;
2692 }
2693
2694 int restrict_rec(int r) {
2695 BddCacheDataI entry;
2696 int res;
2697
2698 if (ISCONST(r) || LEVEL(r) > quantlast)
2699 return r;
2700
2701 entry = BddCache_lookupI(misccache, RESTRHASH(r, miscid));
2702 if (entry.a == r && entry.c == miscid) {
2703 if (CACHESTATS)
2704 cachestats.opHit++;
2705 return entry.res;
2706 }
2707 if (CACHESTATS)
2708 cachestats.opMiss++;
2709
2710 if (INSVARSET(LEVEL(r))) {
2711 if (quantvarset[LEVEL(r)] > 0) {
2712 res = restrict_rec(HIGH(r));
2713 } else {
2714 res = restrict_rec(LOW(r));
2715 }
2716 } else {
2717 PUSHREF(restrict_rec(LOW(r)));
2718 PUSHREF(restrict_rec(HIGH(r)));
2719 res = bdd_makenode(LEVEL(r), READREF(2), READREF(1));
2720 POPREF(2);
2721 }
2722
2723 entry.a = r;
2724 entry.c = miscid;
2725 entry.res = res;
2726
2727 return res;
2728 }
2729
2730 int bdd_simplify(int f, int d) {
2731 int res;
2732 int numReorder = 1;
2733
2734 CHECKa(f, bddfalse);
2735 CHECKa(d, bddfalse);
2736
2737 if (applycache == null) applycache = BddCacheI_init(cachesize);
2738
2739 again : for (;;) {
2740 try {
2741 INITREF();
2742 applyop = bddop_or;
2743
2744 if (numReorder == 0)
2745 bdd_disable_reorder();
2746 res = simplify_rec(f, d);
2747 if (numReorder == 0)
2748 bdd_enable_reorder();
2749 } catch (ReorderException x) {
2750 bdd_checkreorder();
2751
2752 numReorder--;
2753 continue again;
2754 }
2755 break;
2756 }
2757
2758 checkresize();
2759 return res;
2760 }
2761
2762 int simplify_rec(int f, int d) {
2763 BddCacheDataI entry;
2764 int res;
2765
2766 if (ISONE(d) || ISCONST(f))
2767 return f;
2768 if (d == f)
2769 return BDDONE;
2770 if (ISZERO(d))
2771 return BDDZERO;
2772
2773 entry = BddCache_lookupI(applycache, APPLYHASH(f, d, bddop_simplify));
2774
2775 if (entry.a == f && entry.b == d && entry.c == bddop_simplify) {
2776 if (CACHESTATS)
2777 cachestats.opHit++;
2778 return entry.res;
2779 }
2780 if (CACHESTATS)
2781 cachestats.opMiss++;
2782
2783 if (LEVEL(f) == LEVEL(d)) {
2784 if (ISZERO(LOW(d)))
2785 res = simplify_rec(HIGH(f), HIGH(d));
2786 else if (ISZERO(HIGH(d)))
2787 res = simplify_rec(LOW(f), LOW(d));
2788 else {
2789 PUSHREF(simplify_rec(LOW(f), LOW(d)));
2790 PUSHREF(simplify_rec(HIGH(f), HIGH(d)));
2791 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
2792 POPREF(2);
2793 }
2794 } else if (LEVEL(f) < LEVEL(d)) {
2795 PUSHREF(simplify_rec(LOW(f), d));
2796 PUSHREF(simplify_rec(HIGH(f), d));
2797 res = bdd_makenode(LEVEL(f), READREF(2), READREF(1));
2798 POPREF(2);
2799 } else
2800 PUSHREF(or_rec(LOW(d), HIGH(d)));
2801 res = simplify_rec(f, READREF(1));
2802 POPREF(1);
2803 }
2804
2805 entry.a = f;
2806 entry.b = d;
2807 entry.c = bddop_simplify;
2808 entry.res = res;
2809
2810 return res;
2811 }
2812
2813 int supportSize = 0;
2814
2815 int bdd_support(int r) {
2816 int n;
2817 int res = 1;
2818
2819 CHECKa(r, bddfalse);
2820
2821 if (r < 2)
2822 return bddtrue;
2823
2824
2825 if (supportSize < bddvarnum) {
2826 supportSet = new int[bddvarnum];
2827
2828 supportSize = bddvarnum;
2829 supportID = 0;
2830 }
2831
2832
2833
2834
2835
2836
2837
2838 if (supportID == 0x0FFFFFFF) {
2839
2840 for (int i = 0; i < bddvarnum; ++i)
2841 supportSet[i] = 0;
2842 supportID = 0;
2843 }
2844 ++supportID;
2845 supportMin = LEVEL(r);
2846 supportMax = supportMin;
2847
2848 if (ZDD)
2849 zsupport_rec(r, 0, supportSet);
2850 else
2851 support_rec(r, supportSet);
2852 bdd_unmark(r);
2853
2854 bdd_disable_reorder();
2855
2856 for (n = supportMax; n >= supportMin; --n)
2857 if (supportSet[n] == supportID) {
2858 int tmp;
2859 bdd_addref(res);
2860 tmp = makenode_impl(n, 0, res);
2861 bdd_delref(res);
2862 res = tmp;
2863 }
2864
2865 bdd_enable_reorder();
2866
2867 return res;
2868 }
2869
2870 void support_rec(int r, int[] support) {
2871
2872 if (VERIFY_ASSERTIONS) _assert(!ZDD);
2873
2874 if (r < 2)
2875 return;
2876
2877 if (MARKED(r) || LOW(r) == INVALID_BDD)
2878 return;
2879
2880 support[LEVEL(r)] = supportID;
2881
2882 if (LEVEL(r) > supportMax)
2883 supportMax = LEVEL(r);
2884
2885 SETMARK(r);
2886
2887 support_rec(LOW(r), support);
2888 support_rec(HIGH(r), support);
2889 }
2890
2891 void zsupport_rec(int r, int lev, int[] support) {
2892
2893 if (VERIFY_ASSERTIONS) _assert(ZDD);
2894
2895 if (!ISZERO(r)) {
2896 while (lev != LEVEL(r)) {
2897 if (lev > supportMax)
2898 supportMax = lev;
2899 support[lev++] = supportID;
2900 }
2901 }
2902
2903 if (r < 2)
2904 return;
2905
2906 if (MARKED(r) || LOW(r) == INVALID_BDD)
2907 return;
2908
2909 if (LOW(r) == HIGH(r)) {
2910 SETMARK(r);
2911 zsupport_rec(LOW(r), LEVEL(r)+1, support);
2912 return;
2913 }
2914
2915 support[LEVEL(r)] = supportID;
2916
2917 if (LEVEL(r) > supportMax)
2918 supportMax = LEVEL(r);
2919
2920 SETMARK(r);
2921
2922 zsupport_rec(LOW(r), LEVEL(r)+1, support);
2923 zsupport_rec(HIGH(r), LEVEL(r)+1, support);
2924 }
2925
2926 int bdd_appall(int l, int r, int opr, int var) {
2927 int res;
2928 int numReorder = 1;
2929
2930 CHECKa(l, bddfalse);
2931 CHECKa(r, bddfalse);
2932 CHECKa(var, bddfalse);
2933
2934 if (opr < 0 || opr > bddop_invimp) {
2935 bdd_error(BDD_OP);
2936 return bddfalse;
2937 }
2938
2939 if (var < 2)
2940 return bdd_apply(l, r, opr);
2941
2942 if (applycache == null) applycache = BddCacheI_init(cachesize);
2943 if (appexcache == null) appexcache = BddCacheI_init(cachesize);
2944 if (quantcache == null) quantcache = BddCacheI_init(cachesize);
2945
2946 again : for (;;) {
2947 if (varset2vartable(var) < 0)
2948 return bddfalse;
2949 try {
2950 INITREF();
2951 applyop = bddop_and;
2952 appexop = opr;
2953 appexid = (var << 5) | (appexop << 1) | 1;
2954 quantid = (appexid << 3) | CACHEID_APPAL;
2955
2956 if (numReorder == 0)
2957 bdd_disable_reorder();
2958 res = appquant_rec(l, r);
2959 if (numReorder == 0)
2960 bdd_enable_reorder();
2961 } catch (ReorderException x) {
2962 bdd_checkreorder();
2963
2964 numReorder--;
2965 continue again;
2966 }
2967 break;
2968 }
2969
2970 checkresize();
2971 return res;
2972 }
2973
2974 int bdd_appuni(int l, int r, int opr, int var) {
2975 int res;
2976 int numReorder = 1;
2977
2978 CHECKa(l, bddfalse);
2979 CHECKa(r, bddfalse);
2980 CHECKa(var, bddfalse);
2981
2982 if (opr < 0 || opr > bddop_invimp) {
2983 bdd_error(BDD_OP);
2984 return bddfalse;
2985 }
2986
2987 if (var < 2)
2988 return bdd_apply(l, r, opr);
2989
2990 if (applycache == null) applycache = BddCacheI_init(cachesize);
2991 if (appexcache == null) appexcache = BddCacheI_init(cachesize);
2992 if (quantcache == null) quantcache = BddCacheI_init(cachesize);
2993
2994 again : for (;;) {
2995 try {
2996 INITREF();
2997 applyop = bddop_xor;
2998 appexop = opr;
2999 appexid = (var << 5) | (appexop << 1) | 1;
3000 quantid = (appexid << 3) | CACHEID_APPUN;
3001
3002 if (numReorder == 0)
3003 bdd_disable_reorder();
3004 res = appuni_rec(l, r, var);
3005 if (numReorder == 0)
3006 bdd_enable_reorder();
3007 } catch (ReorderException x) {
3008 bdd_checkreorder();
3009 numReorder--;
3010 continue again;
3011 }
3012 break;
3013 }
3014
3015 checkresize();
3016 return res;
3017 }
3018
3019 int bdd_satone(int r) {
3020 int res;
3021
3022 CHECKa(r, bddfalse);
3023 if (r < 2)
3024 return r;
3025
3026 bdd_disable_reorder();
3027
3028 INITREF();
3029 res = satone_rec(r);
3030
3031 bdd_enable_reorder();
3032
3033 checkresize();
3034 return res;
3035 }
3036
3037 int satone_rec(int r) {
3038 if (ISCONST(r))
3039 return r;
3040
3041 if (ISZERO(LOW(r))) {
3042 int res = satone_rec(HIGH(r));
3043 int m = makenode_impl(LEVEL(r), BDDZERO, res);
3044 PUSHREF(m);
3045 return m;
3046 } else {
3047 int res = satone_rec(LOW(r));
3048 int m = makenode_impl(LEVEL(r), res, (ZDD && LOW(r)==HIGH(r))?res:BDDZERO);
3049 PUSHREF(m);
3050 return m;
3051 }
3052 }
3053
3054 int bdd_satoneset(int r, int var, boolean pol) {
3055 int res;
3056
3057 CHECKa(r, bddfalse);
3058 if (ISZERO(r))
3059 return r;
3060
3061 bdd_disable_reorder();
3062
3063 INITREF();
3064 satPolarity = pol;
3065 res = satoneset_rec(r, var);
3066
3067 bdd_enable_reorder();
3068
3069 checkresize();
3070 return res;
3071 }
3072
3073 int satoneset_rec(int r, int var) {
3074 if (ISCONST(r) && ISCONST(var))
3075 return r;
3076
3077 if (LEVEL(r) < LEVEL(var)) {
3078
3079 if (ISZERO(LOW(r))) {
3080 int res = satoneset_rec(HIGH(r), var);
3081 int m = makenode_impl(LEVEL(r), BDDZERO, res);
3082 PUSHREF(m);
3083 return m;
3084 } else {
3085 int res = satoneset_rec(LOW(r), var);
3086 int m = makenode_impl(LEVEL(r), res, (ZDD && LOW(r) == HIGH(r))?res:BDDZERO);
3087 PUSHREF(m);
3088 return m;
3089 }
3090 } else if (LEVEL(var) < LEVEL(r)) {
3091 int res = satoneset_rec(r, HIGH(var));
3092 if (!ZDD && satPolarity) {
3093 int m = makenode_impl(LEVEL(var), BDDZERO, res);
3094 PUSHREF(m);
3095 return m;
3096 } else {
3097 int m = makenode_impl(LEVEL(var), res, BDDZERO);
3098 PUSHREF(m);
3099 return m;
3100 }
3101 } else
3102 if (ISZERO(LOW(r))) {
3103 int res = satoneset_rec(HIGH(r), HIGH(var));
3104 int m = makenode_impl(LEVEL(r), BDDZERO, res);
3105 PUSHREF(m);
3106 return m;
3107 } else {
3108 int res = satoneset_rec(LOW(r), HIGH(var));
3109 int m;
3110 if (ZDD && satPolarity && LOW(r) == HIGH(r))
3111 m = zdd_makenode(LEVEL(r), BDDZERO, res);
3112 else
3113 m = makenode_impl(LEVEL(r), res, BDDZERO);
3114 PUSHREF(m);
3115 return m;
3116 }
3117 }
3118
3119 }
3120
3121 int bdd_fullsatone(int r) {
3122 int res;
3123 int v;
3124
3125 CHECKa(r, bddfalse);
3126 if (r == 0)
3127 return 0;
3128
3129 bdd_disable_reorder();
3130
3131 INITREF();
3132 res = fullsatone_rec(r);
3133
3134 for (v = LEVEL(r) - 1; v >= 0; v--) {
3135 res = PUSHREF(makenode_impl(v, res, 0));
3136 }
3137
3138 bdd_enable_reorder();
3139
3140 checkresize();
3141 return res;
3142 }
3143
3144 int fullsatone_rec(int r) {
3145 if (r < 2)
3146 return r;
3147
3148 if (LOW(r) != 0) {
3149 int res = fullsatone_rec(LOW(r));
3150 int v;
3151
3152 for (v = LEVEL(LOW(r)) - 1; v > LEVEL(r); v--) {
3153 res = PUSHREF(makenode_impl(v, res, 0));
3154 }
3155
3156 return PUSHREF(makenode_impl(LEVEL(r), res, 0));
3157 } else {
3158 int res = fullsatone_rec(HIGH(r));
3159 int v;
3160
3161 for (v = LEVEL(HIGH(r)) - 1; v > LEVEL(r); v--) {
3162 res = PUSHREF(makenode_impl(v, res, 0));
3163 }
3164
3165 return PUSHREF(makenode_impl(LEVEL(r), 0, res));
3166 }
3167 }
3168
3169 void bdd_gbc_rehash() {
3170 int n;
3171
3172 bddfreepos = 0;
3173 bddfreenum = 0;
3174
3175 for (n = bddnodesize - 1; n >= 2; n--) {
3176 if (LOW(n) != INVALID_BDD) {
3177 int hash2;
3178
3179 hash2 = NODEHASH(LEVEL(n), LOW(n), HIGH(n));
3180 SETNEXT(n, HASH(hash2));
3181 SETHASH(hash2, n);
3182 } else {
3183 SETNEXT(n, bddfreepos);
3184 bddfreepos = n;
3185 bddfreenum++;
3186 }
3187 }
3188 }
3189
3190 long clock() {
3191 return System.currentTimeMillis();
3192 }
3193
3194 void INITREF() {
3195 bddrefstacktop = 0;
3196 }
3197 int PUSHREF(int a) {
3198 bddrefstack[bddrefstacktop++] = a;
3199 return a;
3200 }
3201 int READREF(int a) {
3202 return bddrefstack[bddrefstacktop - a];
3203 }
3204 void POPREF(int a) {
3205 bddrefstacktop -= a;
3206 }
3207
3208 int bdd_nodecount(int r) {
3209 int[] num = new int[1];
3210
3211 CHECK(r);
3212
3213 bdd_markcount(r, num);
3214 bdd_unmark(r);
3215
3216 return num[0];
3217 }
3218
3219 int bdd_anodecount(int[] r) {
3220 int n;
3221 int[] cou = new int[1];
3222
3223 for (n = 0; n < r.length; n++)
3224 bdd_markcount(r[n], cou);
3225
3226 for (n = 0; n < r.length; n++)
3227 bdd_unmark(r[n]);
3228
3229 return cou[0];
3230 }
3231
3232 int[] bdd_varprofile(int r) {
3233 CHECK(r);
3234
3235 int[] varprofile = new int[bddvarnum];
3236
3237 varprofile_rec(r, varprofile);
3238 bdd_unmark(r);
3239 return varprofile;
3240 }
3241
3242 void varprofile_rec(int r, int[] varprofile) {
3243
3244 if (r < 2)
3245 return;
3246
3247 if (MARKED(r))
3248 return;
3249
3250 varprofile[bddlevel2var[LEVEL(r)]]++;
3251 SETMARK(r);
3252
3253 varprofile_rec(LOW(r), varprofile);
3254 varprofile_rec(HIGH(r), varprofile);
3255 }
3256
3257 double bdd_pathcount(int r) {
3258 CHECK(r);
3259
3260 miscid = CACHEID_PATHCOU;
3261
3262 if (countcache == null) countcache = BddCacheD_init(cachesize);
3263
3264 return bdd_pathcount_rec(r);
3265 }
3266
3267 double bdd_pathcount_rec(int r) {
3268 BddCacheDataD entry;
3269 double size;
3270
3271 if (ISZERO(r))
3272 return 0.0;
3273 if (ISONE(r))
3274 return 1.0;
3275
3276 entry = BddCache_lookupD(countcache, PATHCOUHASH(r));
3277 if (entry.a == r && entry.c == miscid)
3278 return entry.dres;
3279
3280 size = bdd_pathcount_rec(LOW(r)) + bdd_pathcount_rec(HIGH(r));
3281
3282 entry.a = r;
3283 entry.c = miscid;
3284 entry.dres = size;
3285
3286 return size;
3287 }
3288
3289 double bdd_satcount(int r) {
3290 if (ZDD)
3291 return bdd_pathcount(r);
3292
3293 double size = 1;
3294
3295 CHECK(r);
3296
3297 if (countcache == null) countcache = BddCacheD_init(cachesize);
3298
3299 miscid = CACHEID_SATCOU;
3300 if (!ZDD)
3301 size = Math.pow(2.0, (double) LEVEL(r));
3302
3303 return size * satcount_rec(r);
3304 }
3305
3306 double bdd_satcountset(int r, int varset) {
3307 double unused = bddvarnum;
3308 int n;
3309
3310 if (ISCONST(varset) || ISZERO(r))
3311 return 0.0;
3312
3313 for (n = varset; !ISCONST(n); n = HIGH(n))
3314 unused--;
3315
3316 unused = bdd_satcount(r) / Math.pow(2.0, unused);
3317
3318 return unused >= 1.0 ? unused : 1.0;
3319 }
3320
3321 double satcount_rec(int root) {
3322 BddCacheDataD entry;
3323 double size, s;
3324
3325 if (root < 2)
3326 return root;
3327
3328 entry = BddCache_lookupD(countcache, SATCOUHASH(root));
3329 if (entry.a == root && entry.c == miscid)
3330 return entry.dres;
3331
3332 size = 0;
3333 s = 1;
3334 if (!ZDD)
3335 s *= Math.pow(2.0, (float) (LEVEL(LOW(root)) - LEVEL(root) - 1));
3336 size += s * satcount_rec(LOW(root));
3337
3338 s = 1;
3339 if (!ZDD)
3340 s *= Math.pow(2.0, (float) (LEVEL(HIGH(root)) - LEVEL(root) - 1));
3341 size += s * satcount_rec(HIGH(root));
3342
3343 entry.a = root;
3344 entry.c = miscid;
3345 entry.dres = size;
3346
3347 return size;
3348 }
3349
3350 void bdd_gbc() {
3351 int r;
3352 int n;
3353 long c2, c1 = clock();
3354
3355
3356 {
3357 gcstats.nodes = bddnodesize;
3358 gcstats.freenodes = bddfreenum;
3359 gcstats.time = 0;
3360 gcstats.sumtime = gbcclock;
3361 gcstats.num = gbcollectnum;
3362 gbc_handler(true, gcstats);
3363 }
3364
3365
3366 handleDeferredFree();
3367
3368 for (r = 0; r < bddrefstacktop; r++)
3369 bdd_mark(bddrefstack[r]);
3370
3371 for (n = 0; n < bddnodesize; n++) {
3372 if (HASREF(n))
3373 bdd_mark(n);
3374 SETHASH(n, 0);
3375 }
3376
3377 bddfreepos = 0;
3378 bddfreenum = 0;
3379
3380 for (n = bddnodesize - 1; n >= 2; n--) {
3381
3382 if (MARKED(n) && LOW(n) != INVALID_BDD) {
3383 int hash2;
3384
3385 UNMARK(n);
3386 hash2 = NODEHASH(LEVEL(n), LOW(n), HIGH(n));
3387 SETNEXT(n, HASH(hash2));
3388 SETHASH(hash2, n);
3389 } else {
3390 SETLOW(n, INVALID_BDD);
3391 SETNEXT(n, bddfreepos);
3392 bddfreepos = n;
3393 bddfreenum++;
3394 }
3395 }
3396
3397 if (FLUSH_CACHE_ON_GC) {
3398 bdd_operator_reset();
3399 } else {
3400 bdd_operator_clean();
3401 }
3402
3403 c2 = clock();
3404 gbcclock += c2 - c1;
3405 gbcollectnum++;
3406
3407
3408 {
3409 gcstats.nodes = bddnodesize;
3410 gcstats.freenodes = bddfreenum;
3411 gcstats.time = c2 - c1;
3412 gcstats.sumtime = gbcclock;
3413 gcstats.num = gbcollectnum;
3414 gbc_handler(false, gcstats);
3415 }
3416
3417
3418 }
3419
3420 int bdd_addref(int root) {
3421 if (root == INVALID_BDD)
3422 bdd_error(BDD_BREAK);
3423 if (root < 2 || !bddrunning)
3424 return root;
3425 if (root >= bddnodesize)
3426 return bdd_error(BDD_ILLBDD);
3427 if (LOW(root) == INVALID_BDD)
3428 return bdd_error(BDD_ILLBDD);
3429
3430 INCREF(root);
3431 if (false) System.out.println("INCREF("+root+") = "+GETREF(root));
3432 return root;
3433 }
3434
3435 int bdd_delref(int root) {
3436 if (root == INVALID_BDD)
3437 bdd_error(BDD_BREAK);
3438 if (root < 2 || !bddrunning)
3439 return root;
3440 if (root >= bddnodesize)
3441 return bdd_error(BDD_ILLBDD);
3442 if (LOW(root) == INVALID_BDD)
3443 return bdd_error(BDD_ILLBDD);
3444
3445
3446 if (!HASREF(root))
3447 bdd_error(BDD_BREAK);
3448
3449 DECREF(root);
3450 if (false) System.out.println("DECREF("+root+") = "+GETREF(root));
3451 return root;
3452 }
3453
3454 void bdd_mark(int i) {
3455
3456 if (i < 2)
3457 return;
3458
3459 if (MARKED(i) || LOW(i) == INVALID_BDD)
3460 return;
3461
3462 SETMARK(i);
3463
3464 bdd_mark(LOW(i));
3465 bdd_mark(HIGH(i));
3466 }
3467
3468 void bdd_markcount(int i, int[] cou) {
3469
3470 if (i < 2)
3471 return;
3472
3473 if (MARKED(i) || LOW(i) == INVALID_BDD)
3474 return;
3475
3476 SETMARK(i);
3477 cou[0] += 1;
3478
3479 bdd_markcount(LOW(i), cou);
3480 bdd_markcount(HIGH(i), cou);
3481 }
3482
3483 void bdd_unmark(int i) {
3484
3485 if (i < 2)
3486 return;
3487
3488 if (!MARKED(i) || LOW(i) == INVALID_BDD)
3489 return;
3490 UNMARK(i);
3491
3492 bdd_unmark(LOW(i));
3493 bdd_unmark(HIGH(i));
3494 }
3495
3496 int bdd_makenode(int level, int low, int high) {
3497 if (VERIFY_ASSERTIONS) _assert(!ZDD);
3498
3499 if (CACHESTATS)
3500 cachestats.uniqueAccess++;
3501
3502
3503 if (low == high)
3504 return low;
3505
3506 return makenode(level, low, high);
3507 }
3508
3509 int zdd_makenode(int level, int low, int high) {
3510 if (VERIFY_ASSERTIONS) _assert(ZDD);
3511
3512 if (CACHESTATS)
3513 cachestats.uniqueAccess++;
3514
3515
3516 if (high == 0)
3517 return low;
3518
3519 return makenode(level, low, high);
3520 }
3521
3522
3523 private int makenode(int level, int low, int high) {
3524 int hash2;
3525 int res;
3526
3527
3528 hash2 = NODEHASH(level, low, high);
3529 res = HASH(hash2);
3530
3531 while (res != 0) {
3532 if (LEVEL(res) == level && LOW(res) == low && HIGH(res) == high) {
3533 if (CACHESTATS)
3534 cachestats.uniqueHit++;
3535 return res;
3536 }
3537
3538 res = NEXT(res);
3539 if (CACHESTATS)
3540 cachestats.uniqueChain++;
3541 }
3542
3543
3544 if (CACHESTATS)
3545 cachestats.uniqueMiss++;
3546
3547
3548 if (bddfreepos == 0) {
3549 if (bdderrorcond != 0)
3550 return 0;
3551
3552
3553 bdd_gbc();
3554
3555 if ((bddnodesize-bddfreenum) >= usednodes_nextreorder &&
3556 bdd_reorder_ready())
3557 {
3558 throw new ReorderException();
3559 }
3560
3561 if ((bddfreenum * 100) / bddnodesize <= minfreenodes) {
3562 bdd_noderesize(true);
3563 hash2 = NODEHASH(level, low, high);
3564 }
3565
3566
3567 if (bddfreepos == 0) {
3568 bdd_error(BDD_NODENUM);
3569 bdderrorcond = Math.abs(BDD_NODENUM);
3570 return 0;
3571 }
3572 }
3573
3574
3575 res = bddfreepos;
3576 bddfreepos = NEXT(bddfreepos);
3577 bddfreenum--;
3578 bddproduced++;
3579
3580 SETLEVELANDMARK(res, level);
3581 SETLOW(res, low);
3582 SETHIGH(res, high);
3583
3584
3585 SETNEXT(res, HASH(hash2));
3586 SETHASH(hash2, res);
3587
3588 return res;
3589 }
3590
3591 int bdd_noderesize(boolean doRehash) {
3592 int oldsize = bddnodesize;
3593 int newsize = bddnodesize;
3594
3595 if (bddmaxnodesize > 0) {
3596 if (newsize >= bddmaxnodesize)
3597 return -1;
3598 }
3599
3600 if (increasefactor > 0) {
3601 newsize += (int)(newsize * increasefactor);
3602 } else {
3603 newsize = newsize << 1;
3604 }
3605
3606 if (bddmaxnodeincrease > 0) {
3607 if (newsize > oldsize + bddmaxnodeincrease)
3608 newsize = oldsize + bddmaxnodeincrease;
3609 }
3610
3611 if (bddmaxnodesize > 0) {
3612 if (newsize > bddmaxnodesize)
3613 newsize = bddmaxnodesize;
3614 }
3615
3616 return doResize(doRehash, oldsize, newsize);
3617 }
3618
3619 int doResize(boolean doRehash, int oldsize, int newsize) {
3620
3621 newsize = bdd_prime_lte(newsize);
3622
3623 if (oldsize > newsize) return 0;
3624
3625 resize_handler(oldsize, newsize);
3626
3627 int[] newnodes;
3628 int n;
3629 newnodes = new int[newsize*__node_size];
3630 System.arraycopy(bddnodes, 0, newnodes, 0, bddnodes.length);
3631 bddnodes = newnodes;
3632 bddnodesize = newsize;
3633
3634 if (doRehash)
3635 for (n = 0; n < oldsize; n++)
3636 SETHASH(n, 0);
3637
3638 for (n = oldsize; n < bddnodesize; n++) {
3639 SETLOW(n, INVALID_BDD);
3640
3641
3642
3643 SETNEXT(n, n+1);
3644 }
3645 SETNEXT(bddnodesize-1, bddfreepos);
3646 bddfreepos = oldsize;
3647 bddfreenum += bddnodesize - oldsize;
3648
3649 if (doRehash)
3650 bdd_gbc_rehash();
3651
3652 bddresized = true;
3653
3654 return 0;
3655 }
3656
3657 void bdd_init(int initnodesize, int cs) {
3658 int n;
3659
3660 if (bddrunning)
3661 bdd_error(BDD_RUNNING);
3662
3663 bddnodesize = bdd_prime_gte(initnodesize);
3664
3665 bddnodes = new int[bddnodesize*__node_size];
3666
3667 bddresized = false;
3668
3669 for (n = 0; n < bddnodesize; n++) {
3670 SETLOW(n, INVALID_BDD);
3671
3672
3673
3674 SETNEXT(n, n+1);
3675 }
3676 SETNEXT(bddnodesize-1, 0);
3677
3678 SETMAXREF(0);
3679 SETMAXREF(1);
3680 SETLOW(0, 0); SETHIGH(0, 0);
3681 SETLOW(1, 1); SETHIGH(1, 1);
3682
3683 bdd_operator_init(cs);
3684
3685 bddfreepos = 2;
3686 bddfreenum = bddnodesize - 2;
3687 bddrunning = true;
3688 bddvarnum = 0;
3689 gbcollectnum = 0;
3690 gbcclock = 0;
3691 cachesize = cs;
3692 usednodes_nextreorder = bddnodesize;
3693 bddmaxnodeincrease = DEFAULTMAXNODEINC;
3694
3695 bdderrorcond = 0;
3696
3697 if (CACHESTATS) {
3698
3699 }
3700
3701
3702
3703
3704 bdd_pairs_init();
3705 bdd_reorder_init();
3706
3707 return;
3708 }
3709
3710
3711 static final int CACHEID_CONSTRAIN = 0x0;
3712 static final int CACHEID_RESTRICT = 0x1;
3713 static final int CACHEID_SATCOU = 0x2;
3714 static final int CACHEID_SATCOULN = 0x3;
3715 static final int CACHEID_PATHCOU = 0x4;
3716
3717
3718 static final int CACHEID_REPLACE = 0x0;
3719 static final int CACHEID_COMPOSE = 0x1;
3720 static final int CACHEID_VECCOMPOSE = 0x2;
3721
3722
3723 static final int CACHEID_EXIST = 0x0;
3724 static final int CACHEID_FORALL = 0x1;
3725 static final int CACHEID_UNIQUE = 0x2;
3726 static final int CACHEID_APPEX = 0x3;
3727 static final int CACHEID_APPAL = 0x4;
3728 static final int CACHEID_APPUN = 0x5;
3729
3730
3731 static final int OPERATOR_NUM = 11;
3732
3733
3734 static int oprres[][] =
3735 { { 0, 0, 0, 1 },
3736 0, 1, 1, 0 },
3737 0, 1, 1, 1 },
3738 1, 1, 1, 0 },
3739 1, 0, 0, 0 },
3740 1, 1, 0, 1 },
3741 1, 0, 0, 1 },
3742 0, 0, 1, 0 },
3743 0, 1, 0, 0 },
3744 1, 0, 1, 1 },
3745 1, 1, 0, 0 }
3746 };
3747
3748 int applyop;
3749 int appexop;
3750 int appexid;
3751 int quantid;
3752 int[] quantvarset;
3753 int quantvarsetID;
3754 int quantlast;
3755 int replaceid;
3756 int[] replacepair;
3757 int replacelast;
3758 int composelevel;
3759 int miscid;
3760 int supportID;
3761 int supportMin;
3762 int supportMax;
3763 int[] supportSet;
3764 BddCache applycache;
3765 BddCache itecache;
3766 BddCache quantcache;
3767 BddCache appexcache;
3768 BddCache replacecache;
3769 BddCache misccache;
3770 BddCache countcache;
3771 int cacheratio;
3772 boolean satPolarity;
3773
3774 void bdd_operator_init(int cachesize) {
3775 if (false) {
3776 applycache = BddCacheI_init(cachesize);
3777 itecache = BddCacheI_init(cachesize);
3778 quantcache = BddCacheI_init(cachesize);
3779 appexcache = BddCacheI_init(cachesize);
3780 replacecache = BddCacheI_init(cachesize);
3781 misccache = BddCacheI_init(cachesize);
3782 countcache = BddCacheD_init(cachesize);
3783 }
3784
3785 quantvarsetID = 0;
3786 quantvarset = null;
3787 cacheratio = 0;
3788 supportSet = null;
3789 supportSize = 0;
3790 }
3791
3792 void bdd_operator_done() {
3793 if (quantvarset != null) {
3794 free(quantvarset);
3795 quantvarset = null;
3796 }
3797
3798 BddCache_done(applycache); applycache = null;
3799 BddCache_done(itecache); itecache = null;
3800 BddCache_done(quantcache); quantcache = null;
3801 BddCache_done(appexcache); appexcache = null;
3802 BddCache_done(replacecache); replacecache = null;
3803 BddCache_done(misccache); misccache = null;
3804 BddCache_done(countcache); countcache = null;
3805
3806 if (supportSet != null) {
3807 free(supportSet);
3808 supportSet = null;
3809 supportSize = 0;
3810 }
3811 }
3812
3813 void bdd_operator_reset() {
3814 BddCache_reset(applycache);
3815 BddCache_reset(itecache);
3816 BddCache_reset(quantcache);
3817 BddCache_reset(appexcache);
3818 BddCache_reset(replacecache);
3819 BddCache_reset(misccache);
3820 BddCache_reset(countcache);
3821 }
3822
3823 void bdd_operator_clean() {
3824 BddCache_clean_ab(applycache);
3825 BddCache_clean_abc(itecache);
3826 BddCache_clean_a(quantcache);
3827 BddCache_clean_ab(appexcache);
3828 BddCache_clean_ab(replacecache);
3829 BddCache_clean_ab(misccache);
3830 BddCache_clean_d(countcache);
3831 }
3832
3833 void bdd_operator_varresize() {
3834 if (quantvarset != null)
3835 free(quantvarset);
3836
3837 quantvarset = new int[bddvarnum];
3838
3839
3840 quantvarsetID = 0;
3841
3842 BddCache_reset(countcache);
3843 }
3844
3845 int bdd_setcachesize(int newcachesize) {
3846 int old = cachesize;
3847 BddCache_resize(applycache, newcachesize);
3848 BddCache_resize(itecache, newcachesize);
3849 BddCache_resize(quantcache, newcachesize);
3850 BddCache_resize(appexcache, newcachesize);
3851 BddCache_resize(replacecache, newcachesize);
3852 BddCache_resize(misccache, newcachesize);
3853 BddCache_resize(countcache, newcachesize);
3854 return old;
3855 }
3856
3857 void bdd_operator_noderesize() {
3858 if (cacheratio > 0) {
3859 int newcachesize = bddnodesize / cacheratio;
3860
3861 BddCache_resize(applycache, newcachesize);
3862 BddCache_resize(itecache, newcachesize);
3863 BddCache_resize(quantcache, newcachesize);
3864 BddCache_resize(appexcache, newcachesize);
3865 BddCache_resize(replacecache, newcachesize);
3866 BddCache_resize(misccache, newcachesize);
3867 BddCache_resize(countcache, newcachesize);
3868 }
3869 }
3870
3871 BddCache BddCacheI_init(int size) {
3872 int n;
3873
3874 size = bdd_prime_gte(size);
3875
3876 BddCache cache = new BddCache();
3877 cache.table = new BddCacheDataI[size];
3878
3879 for (n = 0; n < size; n++) {
3880 cache.table[n] = new BddCacheDataI();
3881 cache.table[n].a = -1;
3882 }
3883 cache.tablesize = size;
3884
3885 return cache;
3886 }
3887
3888 BddCache BddCacheD_init(int size) {
3889 int n;
3890
3891 size = bdd_prime_gte(size);
3892
3893 BddCache cache = new BddCache();
3894 cache.table = new BddCacheDataD[size];
3895
3896 for (n = 0; n < size; n++) {
3897 cache.table[n] = new BddCacheDataD();
3898 cache.table[n].a = -1;
3899 }
3900 cache.tablesize = size;
3901
3902 return cache;
3903 }
3904
3905 void BddCache_done(BddCache cache) {
3906 if (cache == null) return;
3907
3908 free(cache.table);
3909 cache.table = null;
3910 cache.tablesize = 0;
3911 }
3912
3913 int BddCache_resize(BddCache cache, int newsize) {
3914 if (cache == null) return 0;
3915 int n;
3916
3917 boolean is_d = cache.table instanceof BddCacheDataD[];
3918
3919 free(cache.table);
3920 cache.table = null;
3921
3922 newsize = bdd_prime_gte(newsize);
3923
3924 if (is_d)
3925 cache.table = new BddCacheDataD[newsize];
3926 else
3927 cache.table = new BddCacheDataI[newsize];
3928
3929 for (n = 0; n < newsize; n++) {
3930 if (is_d)
3931 cache.table[n] = new BddCacheDataD();
3932 else
3933 cache.table[n] = new BddCacheDataI();
3934 cache.table[n].a = -1;
3935 }
3936 cache.tablesize = newsize;
3937
3938 return 0;
3939 }
3940
3941 BddCacheDataI BddCache_lookupI(BddCache cache, int hash) {
3942 return (BddCacheDataI) cache.table[Math.abs(hash % cache.tablesize)];
3943 }
3944
3945 BddCacheDataD BddCache_lookupD(BddCache cache, int hash) {
3946 return (BddCacheDataD) cache.table[Math.abs(hash % cache.tablesize)];
3947 }
3948
3949 void BddCache_reset(BddCache cache) {
3950 if (cache == null) return;
3951 int n;
3952 for (n = 0; n < cache.tablesize; n++)
3953 cache.table[n].a = -1;
3954 }
3955
3956 void BddCache_clean_d(BddCache cache) {
3957 if (cache == null) return;
3958 int n;
3959 for (n = 0; n < cache.tablesize; n++) {
3960 int a = cache.table[n].a;
3961 if (a >= 0 && LOW(a) == INVALID_BDD) {
3962 cache.table[n].a = -1;
3963 }
3964 }
3965 }
3966
3967 void BddCache_clean_a(BddCache cache) {
3968 if (cache == null) return;
3969 int n;
3970 for (n = 0; n < cache.tablesize; n++) {
3971 int a = cache.table[n].a;
3972 if (a < 0) continue;
3973 if (LOW(a) == INVALID_BDD ||
3974 LOW(((BddCacheDataI)cache.table[n]).res) == INVALID_BDD) {
3975 cache.table[n].a = -1;
3976 }
3977 }
3978 }
3979
3980 void BddCache_clean_ab(BddCache cache) {
3981 if (cache == null) return;
3982 int n;
3983 for (n = 0; n < cache.tablesize; n++) {
3984 int a = cache.table[n].a;
3985 if (a < 0) continue;
3986 if (LOW(a) == INVALID_BDD ||
3987 (cache.table[n].b != 0 && LOW(cache.table[n].b) == INVALID_BDD) ||
3988 LOW(((BddCacheDataI)cache.table[n]).res) == INVALID_BDD) {
3989 cache.table[n].a = -1;
3990 }
3991 }
3992 }
3993
3994 void BddCache_clean_abc(BddCache cache) {
3995 if (cache == null) return;
3996 int n;
3997 for (n = 0; n < cache.tablesize; n++) {
3998 int a = cache.table[n].a;
3999 if (a < 0) continue;
4000 if (LOW(a) == -1 ||
4001 LOW(cache.table[n].b) == INVALID_BDD ||
4002 LOW(cache.table[n].c) == INVALID_BDD ||
4003 LOW(((BddCacheDataI)cache.table[n]).res) == INVALID_BDD) {
4004 cache.table[n].a = -1;
4005 }
4006 }
4007 }
4008
4009 void bdd_setpair(bddPair pair, int oldvar, int newvar) {
4010 if (pair == null)
4011 return;
4012
4013 if (oldvar < 0 || oldvar > bddvarnum - 1)
4014 bdd_error(BDD_VAR);
4015 if (newvar < 0 || newvar > bddvarnum - 1)
4016 bdd_error(BDD_VAR);
4017
4018 if (ZDD) {
4019
4020 int oldlev = bddvar2level[oldvar], newlev = bddvar2level[newvar];
4021 int newIndex = newlev;
4022 if (LEVEL(pair.result[newIndex]) != newlev) {
4023
4024 for (newIndex = 0; newIndex < bddvarnum; ++newIndex) {
4025 if (LEVEL(pair.result[newIndex]) == newlev) {
4026 break;
4027 }
4028 }
4029 if (VERIFY_ASSERTIONS) _assert(newIndex != bddvarnum);
4030 }
4031 int tmp = pair.result[oldlev];
4032 pair.result[oldlev] = pair.result[newIndex];
4033 pair.result[newIndex] = tmp;
4034
4035 if (newlev > pair.last)
4036 pair.last = newlev;
4037 } else {
4038 bdd_delref(pair.result[bddvar2level[oldvar]]);
4039 pair.result[bddvar2level[oldvar]] = bdd_ithvar(newvar);
4040 }
4041 pair.id = update_pairsid();
4042
4043 if (bddvar2level[oldvar] > pair.last)
4044 pair.last = bddvar2level[oldvar];
4045
4046 return;
4047 }
4048
4049 void bdd_setbddpair(bddPair pair, int oldvar, int newvar) {
4050 int oldlevel;
4051
4052 if (pair == null)
4053 return;
4054
4055 if (ZDD)
4056 throw new BDDException("setbddpair not supported with ZDDs");
4057
4058 CHECK(newvar);
4059 if (oldvar < 0 || oldvar >= bddvarnum)
4060 bdd_error(BDD_VAR);
4061 oldlevel = bddvar2level[oldvar];
4062
4063 bdd_delref(pair.result[oldlevel]);
4064 pair.result[oldlevel] = bdd_addref(newvar);
4065 pair.id = update_pairsid();
4066
4067 if (oldlevel > pair.last)
4068 pair.last = oldlevel;
4069
4070 return;
4071 }
4072
4073 void bdd_resetpair(bddPair p) {
4074 int n;
4075
4076 for (n = 0; n < bddvarnum; n++) {
4077 if (ZDD) {
4078 bdd_delref(p.result[n]);
4079 p.result[n] = bdd_addref(zdd_makenode(n, 0, 1));
4080 } else
4081 p.result[n] = bdd_ithvar(bddlevel2var[n]);
4082 }
4083 p.last = 0;
4084 }
4085
4086 bddPair pairs;
4087 int pairsid;
4088
4089 static final void free(Object o) {
4090 }
4091
4092 /**************************************************************************
4093 *************************************************************************/
4094
4095 void bdd_pairs_init() {
4096 pairsid = 0;
4097 pairs = null;
4098 }
4099
4100 void bdd_pairs_done() {
4101 bddPair p = pairs;
4102 int n;
4103
4104 while (p != null) {
4105 bddPair next = p.next;
4106 for (n = 0; n < bddvarnum; n++)
4107 bdd_delref(p.result[n]);
4108 p.result = null;
4109 free(p.result);
4110 free(p);
4111 p = next;
4112 }
4113 }
4114
4115 int update_pairsid() {
4116 pairsid++;
4117
4118 if (pairsid == (INT_MAX >> 2)) {
4119 bddPair p;
4120 pairsid = 0;
4121 for (p = pairs; p != null; p = p.next)
4122 p.id = pairsid++;
4123
4124 BddCache_reset(replacecache);
4125 }
4126
4127 return pairsid;
4128 }
4129
4130 void bdd_register_pair(bddPair p) {
4131 p.next = pairs;
4132 pairs = p;
4133 }
4134
4135 void bdd_pairs_vardown(int level) {
4136 bddPair p;
4137
4138 for (p = pairs; p != null; p = p.next) {
4139 int tmp;
4140
4141 tmp = p.result[level];
4142 p.result[level] = p.result[level + 1];
4143 p.result[level + 1] = tmp;
4144
4145 if (p.last == level)
4146 p.last++;
4147 }
4148 }
4149
4150 int bdd_pairs_resize(int oldsize, int newsize) {
4151 bddPair p;
4152 int n;
4153
4154 for (p = pairs; p != null; p = p.next) {
4155 int[] new_result = new int[newsize];
4156 System.arraycopy(p.result, 0, new_result, 0, oldsize);
4157 p.result = new_result;
4158
4159 for (n = oldsize; n < newsize; n++)
4160 if (ZDD)
4161 p.result[n] = bdd_addref(zdd_makenode(n, 0, 1));
4162 else
4163 p.result[n] = bdd_ithvar(bddlevel2var[n]);
4164 }
4165
4166 return 0;
4167 }
4168
4169 void bdd_disable_reorder() {
4170 reorderdisabled = 1;
4171 }
4172 void bdd_enable_reorder() {
4173 reorderdisabled = 0;
4174 }
4175 void bdd_checkreorder() {
4176 bdd_reorder_auto();
4177
4178
4179 usednodes_nextreorder = 2 * (bddnodesize - bddfreenum);
4180
4181
4182
4183 if (bdd_reorder_gain() < 20)
4184 usednodes_nextreorder
4185 += (usednodes_nextreorder * (20 - bdd_reorder_gain()))
4186 / 20;
4187 }
4188
4189 boolean bdd_reorder_ready() {
4190 if ((bddreordermethod == BDD_REORDER_NONE)
4191 || (vartree == null)
4192 || (bddreordertimes == 0)
4193 || (reorderdisabled != 0))
4194 return false;
4195 return true;
4196 }
4197
4198 void bdd_reorder(int method) {
4199 BddTree top;
4200 int savemethod = bddreordermethod;
4201 int savetimes = bddreordertimes;
4202
4203 bddreordermethod = method;
4204 bddreordertimes = 1;
4205
4206 if ((top = bddtree_new(-1)) != null) {
4207 if (reorder_init() >= 0) {
4208
4209 usednum_before = bddnodesize - bddfreenum;
4210
4211 top.firstVar = top.firstLevel = 0;
4212 top.lastVar = top.lastLevel = bdd_varnum() - 1;
4213 top.fixed = false;
4214 top.interleaved = false;
4215 top.next = null;
4216 top.nextlevel = vartree;
4217
4218 reorder_block(top, method);
4219 vartree = top.nextlevel;
4220 free(top);
4221
4222 usednum_after = bddnodesize - bddfreenum;
4223
4224 reorder_done();
4225 bddreordermethod = savemethod;
4226 bddreordertimes = savetimes;
4227 }
4228 }
4229 }
4230
4231 BddTree bddtree_new(int id) {
4232 BddTree t = new BddTree();
4233
4234 t.firstVar = t.lastVar = t.firstLevel = t.lastLevel = -1;
4235 t.fixed = true;
4236
4237
4238
4239 t.id = id;
4240 return t;
4241 }
4242
4243 BddTree reorder_block(BddTree t, int method) {
4244 BddTree dis;
4245
4246 if (t == null)
4247 return null;
4248
4249 if (!t.fixed
4250 && t.nextlevel != null) {
4251 switch (method) {
4252 case BDD_REORDER_WIN2 :
4253 t.nextlevel = reorder_win2(t.nextlevel);
4254 break;
4255 case BDD_REORDER_WIN2ITE :
4256 t.nextlevel = reorder_win2ite(t.nextlevel);
4257 break;
4258 case BDD_REORDER_SIFT :
4259 t.nextlevel = reorder_sift(t.nextlevel);
4260 break;
4261 case BDD_REORDER_SIFTITE :
4262 t.nextlevel = reorder_siftite(t.nextlevel);
4263 break;
4264 case BDD_REORDER_WIN3 :
4265 t.nextlevel = reorder_win3(t.nextlevel);
4266 break;
4267 case BDD_REORDER_WIN3ITE :
4268 t.nextlevel = reorder_win3ite(t.nextlevel);
4269 break;
4270 case BDD_REORDER_RANDOM :
4271 t.nextlevel = reorder_random(t.nextlevel);
4272 break;
4273 }
4274 }
4275
4276 for (dis = t.nextlevel; dis != null; dis = dis.next)
4277 reorder_block(dis, method);
4278
4279 if (t.seq != null) {
4280
4281 varseq_qsort(t.seq, 0, t.lastVar-t.firstVar + 1);
4282 t.firstLevel = bddvar2level[t.seq[0]];
4283 t.lastLevel = bddvar2level[t.seq[t.lastVar-t.firstVar]];
4284 }
4285
4286 return t;
4287 }
4288
4289
4290 void varseq_qsort(int[] target, int from, int to) {
4291
4292 int x, i, j;
4293
4294 switch (to - from) {
4295 case 0 :
4296 return;
4297
4298 case 1 :
4299 return;
4300
4301 case 2 :
4302 if (bddvar2level[target[from]] <= bddvar2level[target[from + 1]])
4303 return;
4304 else {
4305 x = target[from];
4306 target[from] = target[from + 1];
4307 target[from + 1] = x;
4308 }
4309 return;
4310 }
4311
4312 int r = target[from];
4313 int s = target[(from + to) / 2];
4314 int t = target[to - 1];
4315
4316 if (bddvar2level[r] <= bddvar2level[s]) {
4317 if (bddvar2level[s] <= bddvar2level[t]) {
4318 } else if (bddvar2level[r] <= bddvar2level[t]) {
4319 target[to - 1] = s;
4320 target[(from + to) / 2] = t;
4321 } else {
4322 target[to - 1] = s;
4323 target[from] = t;
4324 target[(from + to) / 2] = r;
4325 }
4326 } else {
4327 if (bddvar2level[r] <= bddvar2level[t]) {
4328 target[(from + to) / 2] = r;
4329 target[from] = s;
4330 } else if (bddvar2level[s] <= bddvar2level[t]) {
4331 target[to - 1] = r;
4332 target[(from + to) / 2] = t;
4333 target[from] = s;
4334 } else {
4335 target[to - 1] = r;
4336 target[from] = t;
4337 }
4338 }
4339
4340 int mid = target[(from + to) / 2];
4341
4342 for (i = from + 1, j = to - 1; i + 1 != j;) {
4343 if (target[i] == mid) {
4344 target[i] = target[i + 1];
4345 target[i + 1] = mid;
4346 }
4347
4348 x = target[i];
4349
4350 if (x <= mid)
4351 i++;
4352 else {
4353 x = target[--j];
4354 target[j] = target[i];
4355 target[i] = x;
4356 }
4357 }
4358
4359 varseq_qsort(target, from, i);
4360 varseq_qsort(target, i + 1, to);
4361 }
4362
4363 BddTree reorder_win2(BddTree t) {
4364 BddTree dis = t, first = t;
4365
4366 if (t == null)
4367 return t;
4368
4369 if (verbose > 1) {
4370 System.out.println("Win2 start: " + reorder_nodenum() + " nodes");
4371 System.out.flush();
4372 }
4373
4374 while (dis.next != null) {
4375 int best = reorder_nodenum();
4376 blockdown(dis);
4377
4378 if (best < reorder_nodenum()) {
4379 blockdown(dis.prev);
4380 dis = dis.next;
4381 } else if (first == dis)
4382 first = dis.prev;
4383
4384 if (verbose > 1) {
4385 System.out.print(".");
4386 System.out.flush();
4387 }
4388 }
4389
4390 if (verbose > 1) {
4391 System.out.println();
4392 System.out.println("Win2 end: " + reorder_nodenum() + " nodes");
4393 System.out.flush();
4394 }
4395
4396 return first;
4397 }
4398
4399 BddTree reorder_win3(BddTree t) {
4400 BddTree dis = t, first = t;
4401
4402 if (t == null)
4403 return t;
4404
4405 if (verbose > 1) {
4406 System.out.println("Win3 start: " + reorder_nodenum() + " nodes");
4407 System.out.flush();
4408 }
4409
4410 while (dis.next != null) {
4411 BddTree[] f = new BddTree[1];
4412 f[0] = first;
4413 dis = reorder_swapwin3(dis, f);
4414 first = f[0];
4415
4416 if (verbose > 1) {
4417 System.out.print(".");
4418 System.out.flush();
4419 }
4420 }
4421
4422 if (verbose > 1) {
4423 System.out.println();
4424 System.out.println("Win3 end: " + reorder_nodenum() + " nodes");
4425 System.out.flush();
4426 }
4427
4428 return first;
4429 }
4430
4431 BddTree reorder_win3ite(BddTree t) {
4432 BddTree dis = t, first = t;
4433 int lastsize;
4434
4435 if (t == null)
4436 return t;
4437
4438 if (verbose > 1)
4439 System.out.println(
4440 "Win3ite start: " + reorder_nodenum() + " nodes");
4441
4442 do {
4443 lastsize = reorder_nodenum();
4444 dis = first;
4445
4446 while (dis.next != null && dis.next.next != null) {
4447 BddTree[] f = new BddTree[1];
4448 f[0] = first;
4449 dis = reorder_swapwin3(dis, f);
4450 first = f[0];
4451
4452 if (verbose > 1) {
4453 System.out.print(".");
4454 System.out.flush();
4455 }
4456 }
4457
4458 if (verbose > 1)
4459 System.out.println(" " + reorder_nodenum() + " nodes");
4460 }
4461 while (reorder_nodenum() != lastsize);
4462
4463 if (verbose > 1)
4464 System.out.println("Win3ite end: " + reorder_nodenum() + " nodes");
4465
4466 return first;
4467 }
4468
4469 BddTree reorder_swapwin3(BddTree dis, BddTree[] first) {
4470 boolean setfirst = dis.prev == null;
4471 BddTree next = dis;
4472 int best = reorder_nodenum();
4473
4474 if (dis.next.next == null)
4475 blockdown(dis.prev);
4476
4477 if (best < reorder_nodenum()) {
4478 blockdown(dis.prev);
4479 next = dis.next;
4480 } else {
4481 next = dis;
4482 if (setfirst)
4483 first[0] = dis.prev;
4484 }
4485 } else
4486 int pos = 0;
4487 blockdown(dis);
4488 pos++;
4489 if (best > reorder_nodenum()) {
4490 pos = 0;
4491 best = reorder_nodenum();
4492 }
4493
4494 blockdown(dis);
4495 pos++;
4496 if (best > reorder_nodenum()) {
4497 pos = 0;
4498 best = reorder_nodenum();
4499 }
4500
4501 dis = dis.prev.prev;
4502 blockdown(dis);
4503 pos++;
4504 if (best > reorder_nodenum()) {
4505 pos = 0;
4506 best = reorder_nodenum();
4507 }
4508
4509 blockdown(dis);
4510 pos++;
4511 if (best > reorder_nodenum()) {
4512 pos = 0;
4513 best = reorder_nodenum();
4514 }
4515
4516 dis = dis.prev.prev;
4517 blockdown(dis);
4518 pos++;
4519 if (best > reorder_nodenum()) {
4520 pos = 0;
4521 best = reorder_nodenum();
4522 }
4523
4524 if (pos >= 1)
4525 dis = dis.prev;
4526 blockdown(dis);
4527 next = dis;
4528 if (setfirst)
4529 first[0] = dis.prev;
4530 }
4531
4532 if (pos >= 2)
4533 blockdown(dis);
4534 next = dis.prev;
4535 if (setfirst)
4536 first[0] = dis.prev.prev;
4537 }
4538
4539 if (pos >= 3)
4540 dis = dis.prev.prev;
4541 blockdown(dis);
4542 next = dis;
4543 if (setfirst)
4544 first[0] = dis.prev;
4545 }
4546
4547 if (pos >= 4)
4548 blockdown(dis);
4549 next = dis.prev;
4550 if (setfirst)
4551 first[0] = dis.prev.prev;
4552 }
4553
4554 if (pos >= 5)
4555 dis = dis.prev.prev;
4556 blockdown(dis);
4557 next = dis;
4558 if (setfirst)
4559 first[0] = dis.prev;
4560 }
4561 }
4562
4563 return next;
4564 }
4565
4566 BddTree reorder_sift_seq(BddTree t, BddTree seq[], int num) {
4567 BddTree dis;
4568 int n;
4569
4570 if (t == null)
4571 return t;
4572
4573 for (n = 0; n < num; n++) {
4574 long c2, c1 = clock();
4575
4576 if (verbose > 1) {
4577 System.out.print("Sift ");
4578
4579
4580
4581 System.out.print(seq[n].id);
4582 System.out.print(": ");
4583 }
4584
4585 reorder_sift_bestpos(seq[n], num / 2);
4586
4587 if (verbose > 1) {
4588 System.out.println();
4589 System.out.print("> " + reorder_nodenum() + " nodes");
4590 }
4591
4592 c2 = clock();
4593 if (verbose > 1)
4594 System.out.println(
4595 " (" + (float) (c2 - c1) / (float) 1000 + " sec)\n");
4596 }
4597
4598
4599 for (dis = t; dis.prev != null; dis = dis.prev)
4600
4601
4602 return dis;
4603 }
4604
4605 void reorder_sift_bestpos(BddTree blk, int middlePos) {
4606 int best = reorder_nodenum();
4607 int maxAllowed;
4608 int bestpos = 0;
4609 boolean dirIsUp = true;
4610 int n;
4611
4612 if (bddmaxnodesize > 0)
4613 maxAllowed =
4614 MIN(best / 5 + best, bddmaxnodesize - bddmaxnodeincrease - 2);
4615 else
4616 maxAllowed = best / 5 + best;
4617
4618
4619 if (blk.pos > middlePos)
4620 dirIsUp = false;
4621
4622
4623 for (n = 0; n < 2; n++) {
4624 int first = 1;
4625
4626 if (dirIsUp) {
4627 while (blk.prev != null
4628 && (reorder_nodenum() <= maxAllowed || first != 0)) {
4629 first = 0;
4630 blockdown(blk.prev);
4631 bestpos--;
4632
4633 if (verbose > 1) {
4634 System.out.print("-");
4635 System.out.flush();
4636 }
4637
4638 if (reorder_nodenum() < best) {
4639 best = reorder_nodenum();
4640 bestpos = 0;
4641
4642 if (bddmaxnodesize > 0)
4643 maxAllowed =
4644 MIN(
4645 best / 5 + best,
4646 bddmaxnodesize - bddmaxnodeincrease - 2);
4647 else
4648 maxAllowed = best / 5 + best;
4649 }
4650 }
4651 } else {
4652 while (blk.next != null
4653 && (reorder_nodenum() <= maxAllowed || first != 0)) {
4654 first = 0;
4655 blockdown(blk);
4656 bestpos++;
4657
4658 if (verbose > 1) {
4659 System.out.print("+");
4660 System.out.flush();
4661 }
4662
4663 if (reorder_nodenum() < best) {
4664 best = reorder_nodenum();
4665 bestpos = 0;
4666
4667 if (bddmaxnodesize > 0)
4668 maxAllowed =
4669 MIN(
4670 best / 5 + best,
4671 bddmaxnodesize - bddmaxnodeincrease - 2);
4672 else
4673 maxAllowed = best / 5 + best;
4674 }
4675 }
4676 }
4677
4678 if (reorder_nodenum() > maxAllowed && verbose > 1) {
4679 System.out.print("!");
4680 System.out.flush();
4681 }
4682
4683 dirIsUp = !dirIsUp;
4684 }
4685
4686
4687 while (bestpos < 0) {
4688 blockdown(blk);
4689 bestpos++;
4690 }
4691 while (bestpos > 0) {
4692 blockdown(blk.prev);
4693 bestpos--;
4694 }
4695 }
4696
4697 BddTree reorder_random(BddTree t) {
4698 BddTree dis;
4699 BddTree[] seq;
4700 int n, num = 0;
4701
4702 if (t == null)
4703 return t;
4704
4705 for (dis = t; dis != null; dis = dis.next)
4706 num++;
4707 seq = new BddTree[num];
4708 for (dis = t, num = 0; dis != null; dis = dis.next)
4709 seq[num++] = dis;
4710
4711 for (n = 0; n < 4 * num; n++) {
4712 int blk = rng.nextInt(num);
4713 if (seq[blk].next != null)
4714 blockdown(seq[blk]);
4715 }
4716
4717
4718 for (dis = t; dis.prev != null; dis = dis.prev)
4719
4720
4721 free(seq);
4722
4723 if (verbose != 0)
4724 System.out.println("Random order: " + reorder_nodenum() + " nodes");
4725 return dis;
4726 }
4727
4728 static int siftTestCmp(Object aa, Object bb) {
4729 sizePair a = (sizePair) aa;
4730 sizePair b = (sizePair) bb;
4731
4732 if (a.val < b.val)
4733 return -1;
4734 if (a.val > b.val)
4735 return 1;
4736 return 0;
4737 }
4738
4739 static class sizePair {
4740 int val;
4741 BddTree block;
4742 }
4743
4744 BddTree reorder_sift(BddTree t) {
4745 BddTree dis, seq[];
4746 sizePair[] p;
4747 int n, num;
4748
4749 for (dis = t, num = 0; dis != null; dis = dis.next)
4750 dis.pos = num++;
4751
4752 p = new sizePair[num];
4753 seq = new BddTree[num];
4754
4755 for (dis = t, n = 0; dis != null; dis = dis.next, n++) {
4756 int v;
4757
4758
4759 p[n] = new sizePair();
4760 p[n].val = 0;
4761 for (v = dis.firstVar; v <= dis.lastVar; v++)
4762 p[n].val -= levels[v].nodenum;
4763
4764 p[n].block = dis;
4765 }
4766
4767
4768 Arrays.sort(p, 0, num, new Comparator() {
4769
4770 public int compare(Object o1, Object o2) {
4771 return siftTestCmp(o1, o2);
4772 }
4773
4774 });
4775
4776
4777 for (n = 0; n < num; n++)
4778 seq[n] = p[n].block;
4779
4780
4781 t = reorder_sift_seq(t, seq, num);
4782
4783 free(seq);
4784 free(p);
4785
4786 return t;
4787 }
4788
4789 BddTree reorder_siftite(BddTree t) {
4790 BddTree first = t;
4791 int lastsize;
4792 int c = 1;
4793
4794 if (t == null)
4795 return t;
4796
4797 do {
4798 if (verbose > 1)
4799 System.out.println("Reorder " + (c++) + "\n");
4800
4801 lastsize = reorder_nodenum();
4802 first = reorder_sift(first);
4803 } while (reorder_nodenum() != lastsize);
4804
4805 return first;
4806 }
4807
4808 void blockinterleave(BddTree left) {
4809 BddTree right = left.next;
4810
4811 int n;
4812 int leftsize = left.lastVar - left.firstVar;
4813 int rightsize = right.lastVar - right.firstVar;
4814 int[] lseq = left.seq;
4815 int[] rseq = right.seq;
4816 int minsize = Math.min(leftsize, rightsize);
4817 for (n = 0; n <= minsize; ++n) {
4818 while (bddvar2level[lseq[n]] + 1 < bddvar2level[rseq[n]]) {
4819 reorder_varup(rseq[n]);
4820 }
4821 }
4822 outer:
4823 for ( ; n <= rightsize; ++n) {
4824 for (;;) {
4825 BddTree t = left.prev;
4826 if (t == null || !t.interleaved) break outer;
4827 int tsize = t.lastVar - t.firstVar;
4828 if (n <= tsize) {
4829 int[] tseq = t.seq;
4830 while (bddvar2level[tseq[n]] + 1 < bddvar2level[rseq[n]]) {
4831 reorder_varup(rseq[n]);
4832 }
4833 break;
4834 }
4835 }
4836 }
4837 right.next.prev = left;
4838 left.next = right.next;
4839 left.firstVar = Math.min(left.firstVar, right.firstVar);
4840 left.lastVar = Math.max(left.lastVar, right.lastVar);
4841 left.seq = new int[left.lastVar - left.firstVar + 1];
4842 update_seq(left);
4843 }
4844
4845 void blockdown(BddTree left) {
4846 BddTree right = left.next;
4847
4848 int n;
4849 int leftsize = left.lastVar - left.firstVar;
4850 int rightsize = right.lastVar - right.firstVar;
4851 int leftstart = bddvar2level[left.seq[0]];
4852 int[] lseq = left.seq;
4853 int[] rseq = right.seq;
4854
4855
4856 while (bddvar2level[lseq[0]] < bddvar2level[rseq[rightsize]]) {
4857 for (n = 0; n < leftsize; n++) {
4858 if (bddvar2level[lseq[n]] + 1 != bddvar2level[lseq[n + 1]]
4859 && bddvar2level[lseq[n]] < bddvar2level[rseq[rightsize]]) {
4860 reorder_vardown(lseq[n]);
4861 }
4862 }
4863
4864 if (bddvar2level[lseq[leftsize]] < bddvar2level[rseq[rightsize]]) {
4865 reorder_vardown(lseq[leftsize]);
4866 }
4867 }
4868
4869
4870 while (bddvar2level[rseq[0]] > leftstart) {
4871 for (n = rightsize; n > 0; n--) {
4872 if (bddvar2level[rseq[n]] - 1 != bddvar2level[rseq[n - 1]]
4873 && bddvar2level[rseq[n]] > leftstart) {
4874 reorder_varup(rseq[n]);
4875 }
4876 }
4877
4878 if (bddvar2level[rseq[0]] > leftstart)
4879 reorder_varup(rseq[0]);
4880 }
4881
4882
4883 left.next = right.next;
4884 right.prev = left.prev;
4885 left.prev = right;
4886 right.next = left;
4887
4888 if (right.prev != null)
4889 right.prev.next = right;
4890 if (left.next != null)
4891 left.next.prev = left;
4892
4893 n = left.pos;
4894 left.pos = right.pos;
4895 right.pos = n;
4896
4897 left.interleaved = false;
4898 right.interleaved = false;
4899
4900 left.firstLevel = bddvar2level[lseq[0]];
4901 left.lastLevel = bddvar2level[lseq[leftsize]];
4902 right.firstLevel = bddvar2level[rseq[0]];
4903 right.lastLevel = bddvar2level[rseq[rightsize]];
4904 }
4905
4906 BddTree reorder_win2ite(BddTree t) {
4907 BddTree dis, first = t;
4908 int lastsize;
4909 int c = 1;
4910
4911 if (t == null)
4912 return t;
4913
4914 if (verbose > 1)
4915 System.out.println(
4916 "Win2ite start: " + reorder_nodenum() + " nodes");
4917
4918 do {
4919 lastsize = reorder_nodenum();
4920
4921 dis = t;
4922 while (dis.next != null) {
4923 int best = reorder_nodenum();
4924
4925 blockdown(dis);
4926
4927 if (best < reorder_nodenum()) {
4928 blockdown(dis.prev);
4929 dis = dis.next;
4930 } else if (first == dis)
4931 first = dis.prev;
4932 if (verbose > 1) {
4933 System.out.print(".");
4934 System.out.flush();
4935 }
4936 }
4937
4938 if (verbose > 1)
4939 System.out.println(" " + reorder_nodenum() + " nodes");
4940 c++;
4941 }
4942 while (reorder_nodenum() != lastsize);
4943
4944 return first;
4945 }
4946
4947 void bdd_reorder_auto() {
4948 if (!bdd_reorder_ready())
4949 return;
4950
4951 bdd_reorder(bddreordermethod);
4952 bddreordertimes--;
4953 }
4954
4955 int bdd_reorder_gain() {
4956 if (usednum_before == 0)
4957 return 0;
4958
4959 return (100 * (usednum_before - usednum_after)) / usednum_before;
4960 }
4961
4962 void bdd_done() {
4963
4964
4965
4966 bdd_pairs_done();
4967
4968 free(bddnodes);
4969 free(bddrefstack);
4970 free(bddvarset);
4971 free(bddvar2level);
4972 free(bddlevel2var);
4973
4974 bddnodes = null;
4975 bddrefstack = null;
4976 bddvarset = null;
4977 bddvar2level = null;
4978 bddlevel2var = null;
4979
4980 bdd_operator_done();
4981
4982 bddrunning = false;
4983 bddnodesize = 0;
4984 bddmaxnodesize = 0;
4985 bddvarnum = 0;
4986 bddproduced = 0;
4987
4988 univ = 1;
4989
4990
4991
4992
4993 }
4994
4995 int bdd_setmaxnodenum(int size) {
4996 if (size > bddnodesize || size == 0) {
4997 int old = bddmaxnodesize;
4998 bddmaxnodesize = size;
4999 return old;
5000 }
5001
5002 return bdd_error(BDD_NODES);
5003 }
5004
5005 int bdd_setminfreenodes(int mf) {
5006 int old = minfreenodes;
5007
5008 if (mf < 0 || mf > 100)
5009 return bdd_error(BDD_RANGE);
5010
5011 minfreenodes = mf;
5012 return old;
5013 }
5014
5015 int bdd_setmaxincrease(int size) {
5016 int old = bddmaxnodeincrease;
5017
5018 if (size < 0)
5019 return bdd_error(BDD_SIZE);
5020
5021 bddmaxnodeincrease = size;
5022 return old;
5023 }
5024
5025 double increasefactor;
5026
5027 double bdd_setincreasefactor(double x) {
5028 if (x < 0)
5029 return bdd_error(BDD_RANGE);
5030 double old = increasefactor;
5031 increasefactor = x;
5032 return old;
5033 }
5034
5035 int bdd_setcacheratio(int r) {
5036 int old = cacheratio;
5037
5038 if (r <= 0)
5039 return bdd_error(BDD_RANGE);
5040 if (bddnodesize == 0)
5041 return old;
5042
5043 cacheratio = r;
5044 bdd_operator_noderesize();
5045 return old;
5046 }
5047
5048 int bdd_setvarnum(int num) {
5049 int bdv;
5050 int oldbddvarnum = bddvarnum;
5051
5052 if (num < 1 || num > MAXVAR) {
5053 bdd_error(BDD_RANGE);
5054 return bddfalse;
5055 }
5056
5057 if (num < bddvarnum)
5058 return bdd_error(BDD_DECVNUM);
5059 if (num == bddvarnum)
5060 return 0;
5061
5062 bdd_disable_reorder();
5063
5064 if (bddvarset == null) {
5065 bddvarset = new int[num * 2];
5066 bddlevel2var = new int[num + 1];
5067 bddvar2level = new int[num + 1];
5068 } else {
5069 int[] bddvarset2 = new int[num * 2];
5070 System.arraycopy(bddvarset, 0, bddvarset2, 0, bddvarset.length);
5071 bddvarset = bddvarset2;
5072 int[] bddlevel2var2 = new int[num + 1];
5073 System.arraycopy(
5074 bddlevel2var,
5075 0,
5076 bddlevel2var2,
5077 0,
5078 bddlevel2var.length);
5079 bddlevel2var = bddlevel2var2;
5080 int[] bddvar2level2 = new int[num + 1];
5081 System.arraycopy(
5082 bddvar2level,
5083 0,
5084 bddvar2level2,
5085 0,
5086 bddvar2level.length);
5087 bddvar2level = bddvar2level2;
5088 }
5089
5090 if (bddrefstack != null)
5091 free(bddrefstack);
5092 bddrefstack = new int[num * 2 + 1];
5093 bddrefstacktop = 0;
5094
5095 if (ZDD)
5096 bddvarnum = 0;
5097
5098 univ = 1;
5099 for (bdv = bddvarnum; bddvarnum < num; bddvarnum++) {
5100 if (ZDD) {
5101 int res = 1, res_not = 1;
5102 for (int k = num-1; k >= 0; --k) {
5103 int res2 = zdd_makenode(k, (k == bddvarnum)?0:res, res);
5104 INCREF(res2);
5105 DECREF(res);
5106 res = res2;
5107
5108 int res_not2 = (k == bddvarnum) ? res_not : zdd_makenode(k, res_not, res_not);
5109 INCREF(res_not2);
5110 DECREF(res_not);
5111 res_not = res_not2;
5112
5113 if (bdv == bddvarnum) {
5114 int univ2 = zdd_makenode(k, univ, univ);
5115 INCREF(univ2);
5116 DECREF(univ);
5117 univ = univ2;
5118 }
5119 }
5120 bddvarset[bddvarnum * 2] = res;
5121 bddvarset[bddvarnum * 2 + 1] = res_not;
5122 SETMAXREF(univ);
5123 } else {
5124 bddvarset[bddvarnum * 2] = PUSHREF(bdd_makenode(bddvarnum, 0, 1));
5125 bddvarset[bddvarnum * 2 + 1] = bdd_makenode(bddvarnum, 1, 0);
5126 POPREF(1);
5127 }
5128
5129 if (bdderrorcond != 0) {
5130 bddvarnum = bdv;
5131 return -bdderrorcond;
5132 }
5133
5134 SETMAXREF(bddvarset[bddvarnum * 2]);
5135 SETMAXREF(bddvarset[bddvarnum * 2 + 1]);
5136 bddlevel2var[bddvarnum] = bddvarnum;
5137 bddvar2level[bddvarnum] = bddvarnum;
5138 }
5139
5140 SETLEVELANDMARK(0, num);
5141 SETLEVELANDMARK(1, num);
5142 bddvar2level[num] = num;
5143 bddlevel2var[num] = num;
5144
5145 bdd_pairs_resize(oldbddvarnum, bddvarnum);
5146 bdd_operator_varresize();
5147
5148 if (ZDD) {
5149 System.out.println("Changed number of ZDD variables to "+num+", all existing ZDDs are now invalid.");
5150
5151 for (int n = 0; n < fdvarnum; n++) {
5152 domain[n].var.free();
5153 domain[n].var = makeSet(domain[n].ivar);
5154 }
5155 }
5156
5157 bdd_enable_reorder();
5158
5159 return 0;
5160 }
5161
5162 static class BddTree {
5163 int firstVar, lastVar;
5164 int firstLevel, lastLevel;
5165 int pos;
5166 int[] seq;
5167 boolean fixed;
5168 boolean interleaved;
5169 int id;
5170 BddTree next, prev;
5171 BddTree nextlevel;
5172 }
5173
5174
5175 int bddreordermethod;
5176 int bddreordertimes;
5177
5178
5179 int reorderdisabled;
5180
5181 BddTree vartree;
5182 int blockid;
5183
5184 int[] extroots;
5185 int extrootsize;
5186
5187 levelData levels[];
5188
5189 static class levelData {
5190 int start;
5191 int size;
5192 int maxsize;
5193 int nodenum;
5194 }
5195
5196 static class imatrix {
5197 byte rows[][];
5198 int size;
5199 }
5200
5201
5202 imatrix iactmtx;
5203
5204 int verbose;
5205
5206
5207
5208
5209
5210 int usednum_before;
5211 int usednum_after;
5212
5213 void bdd_reorder_init() {
5214 reorderdisabled = 0;
5215 vartree = null;
5216
5217 bdd_clrvarblocks();
5218
5219 bdd_reorder_verbose(0);
5220 bdd_autoreorder_times(BDD_REORDER_NONE, 0);
5221
5222 usednum_before = usednum_after = 0;
5223 blockid = 0;
5224 }
5225
5226 int reorder_nodenum() {
5227 return bdd_getnodenum();
5228 }
5229
5230 int bdd_getnodenum() {
5231 return bddnodesize - bddfreenum;
5232 }
5233
5234 int bdd_reorder_verbose(int v) {
5235 int tmp = verbose;
5236 verbose = v;
5237 return tmp;
5238 }
5239
5240 int bdd_autoreorder(int method) {
5241 int tmp = bddreordermethod;
5242 bddreordermethod = method;
5243 bddreordertimes = -1;
5244 return tmp;
5245 }
5246
5247 int bdd_autoreorder_times(int method, int num) {
5248 int tmp = bddreordermethod;
5249 bddreordermethod = method;
5250 bddreordertimes = num;
5251 return tmp;
5252 }
5253
5254 static final int BDD_REORDER_NONE = 0;
5255 static final int BDD_REORDER_WIN2 = 1;
5256 static final int BDD_REORDER_WIN2ITE = 2;
5257 static final int BDD_REORDER_SIFT = 3;
5258 static final int BDD_REORDER_SIFTITE = 4;
5259 static final int BDD_REORDER_WIN3 = 5;
5260 static final int BDD_REORDER_WIN3ITE = 6;
5261 static final int BDD_REORDER_RANDOM = 7;
5262
5263 static final int BDD_REORDER_FREE = 0;
5264 static final int BDD_REORDER_FIXED = 1;
5265
5266 void bdd_reorder_done() {
5267 bddtree_del(vartree);
5268 bdd_operator_reset();
5269 vartree = null;
5270 }
5271
5272 void bddtree_del(BddTree t) {
5273 if (t == null)
5274 return;
5275
5276 bddtree_del(t.nextlevel);
5277 bddtree_del(t.next);
5278 if (t.seq != null)
5279 free(t.seq);
5280 t.seq = null;
5281 free(t);
5282 }
5283
5284 void bdd_clrvarblocks() {
5285 bddtree_del(vartree);
5286 vartree = null;
5287 blockid = 0;
5288 }
5289
5290 int NODEHASHr(int var, int l, int h) {
5291 return (Math.abs(PAIR(l, (h)) % levels[var].size) + levels[var].start);
5292 }
5293
5294 void bdd_setvarorder(int[] neworder) {
5295 int level;
5296
5297
5298 if (vartree != null) {
5299 bdd_error(BDD_VARBLK);
5300 return;
5301 }
5302
5303 reorder_init();
5304
5305 for (level = 0; level < bddvarnum; level++) {
5306 int lowvar = neworder[level];
5307
5308 while (bddvar2level[lowvar] > level)
5309 reorder_varup(lowvar);
5310 }
5311
5312 reorder_done();
5313 }
5314
5315 int reorder_varup(int var) {
5316 if (var < 0 || var >= bddvarnum)
5317 return bdd_error(BDD_VAR);
5318 if (bddvar2level[var] == 0)
5319 return 0;
5320 return reorder_vardown(bddlevel2var[bddvar2level[var] - 1]);
5321 }
5322
5323 int reorder_vardown(int var) {
5324 int n, level;
5325
5326 if (var < 0 || var >= bddvarnum)
5327 return bdd_error(BDD_VAR);
5328 if ((level = bddvar2level[var]) >= bddvarnum - 1)
5329 return 0;
5330
5331 resizedInMakenode = false;
5332
5333 if (imatrixDepends(iactmtx, var, bddlevel2var[level + 1])) {
5334
5335
5336
5337
5338
5339 int toBeProcessed = reorder_downSimple(var);
5340 levelData l = levels[var];
5341
5342 if (l.nodenum < (l.size) / 3
5343 || l.nodenum >= (l.size * 3) / 2
5344 && l.size < l.maxsize) {
5345
5346 reorder_swapResize(toBeProcessed, var);
5347 reorder_localGbcResize(toBeProcessed, var);
5348 } else {
5349
5350 reorder_swap(toBeProcessed, var);
5351 reorder_localGbc(var);
5352 }
5353 }
5354
5355
5356 n = bddlevel2var[level];
5357 bddlevel2var[level] = bddlevel2var[level + 1];
5358 bddlevel2var[level + 1] = n;
5359
5360 n = bddvar2level[var];
5361 bddvar2level[var] = bddvar2level[bddlevel2var[level]];
5362 bddvar2level[bddlevel2var[level]] = n;
5363
5364
5365 bdd_pairs_vardown(level);
5366
5367 if (resizedInMakenode) {
5368 reorder_rehashAll();
5369 }
5370
5371 return 0;
5372 }
5373
5374 boolean imatrixDepends(imatrix mtx, int a, int b) {
5375 return (mtx.rows[a][b / 8] & (1 << (b % 8))) != 0;
5376 }
5377
5378 void reorder_setLevellookup() {
5379 int n;
5380
5381 for (n = 0; n < bddvarnum; n++) {
5382 levels[n].maxsize = bddnodesize / bddvarnum;
5383 levels[n].start = n * levels[n].maxsize;
5384 levels[n].size =
5385 Math.min(levels[n].maxsize, (levels[n].nodenum * 5) / 4);
5386
5387 if (levels[n].size >= 4)
5388 levels[n].size = bdd_prime_lte(levels[n].size);
5389
5390 }
5391 }
5392
5393 void reorder_rehashAll() {
5394 int n;
5395
5396 reorder_setLevellookup();
5397 bddfreepos = 0;
5398
5399 for (n = bddnodesize - 1; n >= 0; n--)
5400 SETHASH(n, 0);
5401
5402 for (n = bddnodesize - 1; n >= 2; n--) {
5403 if (HASREF(n)) {
5404 int hash2 = NODEHASH2(VARr(n), LOW(n), HIGH(n));
5405 SETNEXT(n, HASH(hash2));
5406 SETHASH(hash2, n);
5407 } else {
5408 SETNEXT(n, bddfreepos);
5409 bddfreepos = n;
5410 }
5411 }
5412 }
5413
5414 void reorder_localGbc(int var0) {
5415 int var1 = bddlevel2var[bddvar2level[var0] + 1];
5416 int vl1 = levels[var1].start;
5417 int size1 = levels[var1].size;
5418 int n;
5419
5420 for (n = 0; n < size1; n++) {
5421 int hash = n + vl1;
5422 int r = HASH(hash);
5423 SETHASH(hash, 0);
5424
5425 while (r != 0) {
5426 int next = NEXT(r);
5427
5428 if (HASREF(r)) {
5429 SETNEXT(r, HASH(hash));
5430 SETHASH(hash, r);
5431 } else {
5432 DECREF(LOW(r));
5433 DECREF(HIGH(r));
5434
5435 SETLOW(r, INVALID_BDD);
5436 SETNEXT(r, bddfreepos);
5437 bddfreepos = r;
5438 levels[var1].nodenum--;
5439 bddfreenum++;
5440 }
5441
5442 r = next;
5443 }
5444 }
5445 }
5446
5447 int reorder_downSimple(int var0) {
5448 int toBeProcessed = 0;
5449
5450
5451 int var1 = bddlevel2var[bddvar2level[var0] + 1];
5452
5453
5454 int vl0 = levels[var0].start;
5455 int size0 = levels[var0].size;
5456 int n;
5457
5458
5459 levels[var0].nodenum = 0;
5460 for (n = 0; n < size0; n++) {
5461 int r;
5462
5463 r = HASH(n + vl0);
5464 SETHASH(n + vl0, 0);
5465
5466 while (r != 0) {
5467 int next = NEXT(r);
5468
5469 if (VARr(LOW(r)) != var1 && VARr(HIGH(r)) != var1) {
5470
5471 SETNEXT(r, HASH(n + vl0));
5472 SETHASH(n + vl0, r);
5473 levels[var0].nodenum++;
5474 } else {
5475
5476 SETNEXT(r, toBeProcessed);
5477 toBeProcessed = r;
5478 if (SWAPCOUNT)
5479 cachestats.swapCount++;
5480 }
5481
5482 r = next;
5483 }
5484 }
5485
5486 return toBeProcessed;
5487 }
5488
5489 void reorder_swapResize(int toBeProcessed, int var0) {
5490 int var1 = bddlevel2var[bddvar2level[var0] + 1];
5491
5492 while (toBeProcessed != 0) {
5493 int next = NEXT(toBeProcessed);
5494 int f0 = LOW(toBeProcessed);
5495 int f1 = HIGH(toBeProcessed);
5496 int f00, f01, f10, f11;
5497
5498
5499 if (VARr(f0) == var1) {
5500 f00 = LOW(f0);
5501 f01 = HIGH(f0);
5502 } else
5503 f00 = f01 = f0;
5504
5505 if (VARr(f1) == var1) {
5506 f10 = LOW(f1);
5507 f11 = HIGH(f1);
5508 } else
5509 f10 = f11 = f1;
5510
5511
5512 f0 = reorder_makenode(var0, f00, f10);
5513 f1 = reorder_makenode(var0, f01, f11);
5514
5515
5516
5517
5518
5519
5520
5521
5522 DECREF(LOW(toBeProcessed));
5523 DECREF(HIGH(toBeProcessed));
5524
5525
5526 SETVARr(toBeProcessed, var1);
5527 SETLOW(toBeProcessed, f0);
5528 SETHIGH(toBeProcessed, f1);
5529
5530 levels[var1].nodenum++;
5531
5532
5533
5534 toBeProcessed = next;
5535 }
5536 }
5537
5538 static final int MIN(int a, int b) {
5539 return Math.min(a, b);
5540 }
5541
5542 void reorder_localGbcResize(int toBeProcessed, int var0) {
5543 int var1 = bddlevel2var[bddvar2level[var0] + 1];
5544 int vl1 = levels[var1].start;
5545 int size1 = levels[var1].size;
5546 int n;
5547
5548 for (n = 0; n < size1; n++) {
5549 int hash = n + vl1;
5550 int r = HASH(hash);
5551 SETHASH(hash, 0);
5552
5553 while (r != 0) {
5554 int next = NEXT(r);
5555
5556 if (HASREF(r)) {
5557 SETNEXT(r, toBeProcessed);
5558 toBeProcessed = r;
5559 } else {
5560 DECREF(LOW(r));
5561 DECREF(HIGH(r));
5562
5563 SETLOW(r, INVALID_BDD);
5564 SETNEXT(r, bddfreepos);
5565 bddfreepos = r;
5566 levels[var1].nodenum--;
5567 bddfreenum++;
5568 }
5569
5570 r = next;
5571 }
5572 }
5573
5574
5575 if (levels[var1].nodenum < levels[var1].size)
5576 levels[var1].size =
5577 MIN(levels[var1].maxsize, levels[var1].size / 2);
5578 else
5579 levels[var1].size =
5580 MIN(levels[var1].maxsize, levels[var1].size * 2);
5581
5582 if (levels[var1].size >= 4)
5583 levels[var1].size = bdd_prime_lte(levels[var1].size);
5584
5585
5586 while (toBeProcessed != 0) {
5587 int next = NEXT(toBeProcessed);
5588 int hash = NODEHASH2(VARr(toBeProcessed), LOW(toBeProcessed), HIGH(toBeProcessed));
5589
5590 SETNEXT(toBeProcessed, HASH(hash));
5591 SETHASH(hash, toBeProcessed);
5592
5593 toBeProcessed = next;
5594 }
5595 }
5596
5597 void reorder_swap(int toBeProcessed, int var0) {
5598 int var1 = bddlevel2var[bddvar2level[var0] + 1];
5599
5600
5601
5602 while (toBeProcessed != 0) {
5603 int next = NEXT(toBeProcessed);
5604 int f0 = LOW(toBeProcessed);
5605 int f1 = HIGH(toBeProcessed);
5606 int f00, f01, f10, f11, hash;
5607
5608
5609 if (VARr(f0) == var1) {
5610 f00 = LOW(f0);
5611 f01 = HIGH(f0);
5612 } else
5613 f00 = f01 = f0;
5614
5615 if (VARr(f1) == var1) {
5616 f10 = LOW(f1);
5617 f11 = HIGH(f1);
5618 } else
5619 f10 = f11 = f1;
5620
5621
5622 f0 = reorder_makenode(var0, f00, f10);
5623 f1 = reorder_makenode(var0, f01, f11);
5624
5625
5626
5627
5628
5629
5630
5631
5632 DECREF(LOW(toBeProcessed));
5633 DECREF(HIGH(toBeProcessed));
5634
5635
5636
5637
5638
5639 SETVARr(toBeProcessed, var1);
5640 SETLOW(toBeProcessed, f0);
5641 SETHIGH(toBeProcessed, f1);
5642
5643 levels[var1].nodenum++;
5644
5645
5646 hash = NODEHASH2(VARr(toBeProcessed), LOW(toBeProcessed), HIGH(toBeProcessed));
5647 SETNEXT(toBeProcessed, HASH(hash));
5648 SETHASH(hash, toBeProcessed);
5649
5650 toBeProcessed = next;
5651 }
5652 }
5653
5654 int NODEHASH2(int var, int l, int h) {
5655 return (Math.abs(PAIR(l, h) % levels[var].size) + levels[var].start);
5656 }
5657
5658 boolean resizedInMakenode;
5659
5660 int reorder_makenode(int var, int low, int high) {
5661 int hash;
5662 int res;
5663
5664 if (CACHESTATS)
5665 cachestats.uniqueAccess++;
5666
5667
5668
5669
5670 if (ZDD) {
5671
5672 if (high == 0) {
5673 INCREF(low);
5674 return low;
5675 }
5676 } else {
5677
5678 if (low == high) {
5679 INCREF(low);
5680 return low;
5681 }
5682 }
5683
5684
5685 hash = NODEHASH2(var, low, high);
5686 res = HASH(hash);
5687
5688 while (res != 0) {
5689 if (LOW(res) == low && HIGH(res) == high) {
5690 if (CACHESTATS)
5691 cachestats.uniqueHit++;
5692 INCREF(res);
5693 return res;
5694 }
5695 res = NEXT(res);
5696
5697 if (CACHESTATS)
5698 cachestats.uniqueChain++;
5699 }
5700
5701
5702 if (CACHESTATS)
5703 cachestats.uniqueMiss++;
5704
5705
5706 if (bddfreepos == 0) {
5707 if (bdderrorcond != 0)
5708 return 0;
5709
5710
5711
5712
5713
5714 bdd_noderesize(false);
5715 resizedInMakenode = true;
5716
5717
5718 if (bddfreepos == 0) {
5719 bdd_error(BDD_NODENUM);
5720 bdderrorcond = Math.abs(BDD_NODENUM);
5721 return 0;
5722 }
5723 }
5724
5725
5726 res = bddfreepos;
5727 bddfreepos = NEXT(bddfreepos);
5728 levels[var].nodenum++;
5729 bddproduced++;
5730 bddfreenum--;
5731
5732 SETVARr(res, var);
5733 SETLOW(res, low);
5734 SETHIGH(res, high);
5735
5736
5737 SETNEXT(res, HASH(hash));
5738 SETHASH(hash, res);
5739
5740
5741 CLEARREF(res);
5742 INCREF(res);
5743 INCREF(LOW(res));
5744 INCREF(HIGH(res));
5745
5746 return res;
5747 }
5748
5749 int reorder_init() {
5750
5751
5752
5753
5754
5755
5756 int n;
5757
5758 reorder_handler(true, reorderstats);
5759
5760
5761 levels = new levelData[bddvarnum];
5762 for (n = 0; n < bddvarnum; n++) {
5763 levels[n] = new levelData();
5764 levels[n].start = -1;
5765 levels[n].size = 0;
5766 levels[n].nodenum = 0;
5767 }
5768
5769
5770
5771 if (mark_roots() < 0)
5772 return -1;
5773
5774
5775 reorder_setLevellookup();
5776
5777
5778 reorder_gbc();
5779
5780 return 0;
5781 }
5782
5783 int mark_roots() {
5784 boolean[] dep = new boolean[bddvarnum];
5785 int n;
5786
5787 for (n = 2, extrootsize = 0; n < bddnodesize; n++) {
5788
5789
5790 SETLEVELANDMARK(n, bddlevel2var[LEVELANDMARK(n)]);
5791
5792 if (HASREF(n)) {
5793 SETMARK(n);
5794 extrootsize++;
5795 }
5796 }
5797
5798 extroots = new int[extrootsize];
5799
5800 iactmtx = imatrixNew(bddvarnum);
5801
5802
5803 for (n = 2, extrootsize = 0; n < bddnodesize; n++) {
5804
5805 if (MARKED(n)) {
5806
5807 UNMARK(n);
5808 extroots[extrootsize++] = n;
5809
5810
5811
5812 for (int i = 0; i < bddvarnum; ++i)
5813 dep[i] = false;
5814
5815 dep[VARr(n)] = true;
5816 levels[VARr(n)].nodenum++;
5817
5818 addref_rec(LOW(n), dep);
5819 addref_rec(HIGH(n), dep);
5820
5821 addDependencies(dep);
5822 }
5823
5824
5825
5826 SETHASH(n, 0);
5827 }
5828
5829 SETHASH(0, 0);
5830 SETHASH(1, 0);
5831
5832 free(dep);
5833 return 0;
5834 }
5835
5836 imatrix imatrixNew(int size) {
5837 imatrix mtx = new imatrix();
5838 int n;
5839
5840 mtx.rows = new byte[size][];
5841
5842 for (n = 0; n < size; n++) {
5843 mtx.rows[n] = new byte[size / 8 + 1];
5844 }
5845
5846 mtx.size = size;
5847
5848 return mtx;
5849 }
5850
5851 void addref_rec(int r, boolean[] dep) {
5852 if (r < 2)
5853 return;
5854
5855 if (!HASREF(r) || MARKED(r)) {
5856
5857
5858
5859 bddfreenum--;
5860
5861
5862 dep[VARr(r) & ~MARK_MASK] = true;
5863
5864
5865 levels[VARr(r) & ~MARK_MASK].nodenum++;
5866
5867 addref_rec(LOW(r), dep);
5868 addref_rec(HIGH(r), dep);
5869 } else {
5870 int n;
5871
5872
5873
5874 for (n = 0; n < bddvarnum; n++)
5875 dep[n]
5876 |= imatrixDepends(iactmtx, VARr(r) & ~MARK_MASK, n);
5877 }
5878
5879 INCREF(r);
5880 }
5881
5882 void addDependencies(boolean[] dep) {
5883 int n, m;
5884
5885 for (n = 0; n < bddvarnum; n++) {
5886 for (m = n; m < bddvarnum; m++) {
5887 if ((dep[n]) && (dep[m])) {
5888 imatrixSet(iactmtx, n, m);
5889 imatrixSet(iactmtx, m, n);
5890 }
5891 }
5892 }
5893 }
5894
5895 void imatrixSet(imatrix mtx, int a, int b) {
5896 mtx.rows[a][b / 8] |= 1 << (b % 8);
5897 }
5898
5899 void reorder_gbc() {
5900 int n;
5901
5902 bddfreepos = 0;
5903 bddfreenum = 0;
5904
5905
5906
5907 for (n = bddnodesize - 1; n >= 2; n--) {
5908
5909 if (HASREF(n)) {
5910 int hash;
5911
5912 hash = NODEHASH2(VARr(n), LOW(n), HIGH(n));
5913 SETNEXT(n, HASH(hash));
5914 SETHASH(hash, n);
5915
5916 } else {
5917 SETLOW(n, INVALID_BDD);
5918 SETNEXT(n, bddfreepos);
5919 bddfreepos = n;
5920 bddfreenum++;
5921 }
5922 }
5923 }
5924
5925 void reorder_done() {
5926 int n;
5927
5928 for (n = 0; n < extrootsize; n++)
5929 SETMARK(extroots[n]);
5930 for (n = 2; n < bddnodesize; n++) {
5931 if (MARKED(n))
5932 UNMARK(n);
5933 else
5934 CLEARREF(n);
5935
5936
5937
5938 SETLEVELANDMARK(n, bddvar2level[LEVELANDMARK(n)]);
5939 }
5940
5941 free(extroots);
5942 free(levels);
5943 imatrixDelete(iactmtx);
5944 bdd_gbc();
5945
5946 reorder_handler(false, reorderstats);
5947 }
5948
5949 void imatrixDelete(imatrix mtx) {
5950 int n;
5951
5952 for (n = 0; n < mtx.size; n++) {
5953 free(mtx.rows[n]);
5954 mtx.rows[n] = null;
5955 }
5956 free(mtx.rows);
5957 mtx.rows = null;
5958 free(mtx);
5959 }
5960
5961 int bdd_getallocnum() {
5962 return bddnodesize;
5963 }
5964
5965 int bdd_setallocnum(int size) {
5966 int old = bddnodesize;
5967 doResize(true, old, size);
5968 return old;
5969 }
5970
5971 int bdd_swapvar(int v1, int v2) {
5972 int l1, l2;
5973
5974
5975 if (vartree != null)
5976 return bdd_error(BDD_VARBLK);
5977
5978
5979 if (v1 == v2)
5980 return 0;
5981
5982
5983 if (v1 < 0 || v1 >= bddvarnum || v2 < 0 || v2 >= bddvarnum)
5984 return bdd_error(BDD_VAR);
5985
5986 l1 = bddvar2level[v1];
5987 l2 = bddvar2level[v2];
5988
5989
5990 if (l1 > l2) {
5991 int tmp = v1;
5992 v1 = v2;
5993 v2 = tmp;
5994 l1 = bddvar2level[v1];
5995 l2 = bddvar2level[v2];
5996 }
5997
5998 reorder_init();
5999
6000
6001 while (bddvar2level[v1] < l2)
6002 reorder_vardown(v1);
6003
6004
6005 while (bddvar2level[v2] > l1)
6006 reorder_varup(v2);
6007
6008 reorder_done();
6009
6010 return 0;
6011 }
6012
6013 void bdd_fprintall(PrintStream out) {
6014 int n;
6015
6016 for (n = 0; n < bddnodesize; n++) {
6017 if (LOW(n) != INVALID_BDD) {
6018 out.print(
6019 "["
6020 + right(n, 5)
6021 + " - "
6022 + right(GETREF(n), 2)
6023 + "] ");
6024
6025 out.print(right(bddlevel2var[LEVEL(n)], 3));
6026
6027 out.print(": " + right(LOW(n), 3));
6028 out.println(" " + right(HIGH(n), 3));
6029 }
6030 }
6031 }
6032
6033 void bdd_fprinttable(PrintStream out, int r) {
6034 int n;
6035
6036 out.println("ROOT: " + r);
6037 if (r < 2)
6038 return;
6039
6040 bdd_mark(r);
6041
6042 for (n = 0; n < bddnodesize; n++) {
6043 if (MARKED(n)) {
6044 UNMARK(n);
6045
6046 out.print("[" + right(n, 5) + "] ");
6047
6048 out.print(right(bddlevel2var[LEVEL(n)], 3));
6049
6050 out.print(": " + right(LOW(n), 3));
6051 out.println(" " + right(HIGH(n), 3));
6052 }
6053 }
6054 }
6055
6056 int lh_nodenum;
6057 int lh_freepos;
6058 int[] loadvar2level;
6059 LoadHash[] lh_table;
6060
6061 int bdd_load(BufferedReader ifile, int[] translate) throws IOException {
6062 int n, vnum, tmproot;
6063 int root;
6064
6065 lh_nodenum = Integer.parseInt(readNext(ifile));
6066 vnum = Integer.parseInt(readNext(ifile));
6067
6068
6069 if (lh_nodenum == 0 && vnum == 0) {
6070 root = Integer.parseInt(readNext(ifile));
6071 return root;
6072 }
6073
6074
6075 loadvar2level = new int[vnum];
6076 for (n = 0; n < vnum; n++) {
6077 loadvar2level[n] = Integer.parseInt(readNext(ifile));
6078 }
6079
6080 if (vnum > bddvarnum)
6081 bdd_setvarnum(vnum);
6082
6083 lh_table = new LoadHash[lh_nodenum];
6084
6085 for (n = 0; n < lh_nodenum; n++) {
6086 lh_table[n] = new LoadHash();
6087 lh_table[n].first = -1;
6088 lh_table[n].next = n + 1;
6089 }
6090 lh_table[lh_nodenum - 1].next = -1;
6091 lh_freepos = 0;
6092
6093 tmproot = bdd_loaddata(ifile, translate);
6094
6095 for (n = 0; n < lh_nodenum; n++)
6096 bdd_delref(lh_table[n].data);
6097
6098 free(lh_table);
6099 lh_table = null;
6100 free(loadvar2level);
6101 loadvar2level = null;
6102
6103 root = tmproot;
6104 return root;
6105 }
6106
6107 static class LoadHash {
6108 int key;
6109 int data;
6110 int first;
6111 int next;
6112 }
6113
6114 int bdd_loaddata(BufferedReader ifile, int[] translate) throws IOException {
6115 int key, var, low, high, root = 0, n;
6116
6117 for (n = 0; n < lh_nodenum; n++) {
6118 key = Integer.parseInt(readNext(ifile));
6119 var = Integer.parseInt(readNext(ifile));
6120 if (translate != null)
6121 var = translate[var];
6122 low = Integer.parseInt(readNext(ifile));
6123 high = Integer.parseInt(readNext(ifile));
6124
6125 if (low >= 2)
6126 low = loadhash_get(low);
6127 if (high >= 2)
6128 high = loadhash_get(high);
6129
6130 if (low < 0 || high < 0 || var < 0)
6131 return bdd_error(BDD_FORMAT);
6132
6133 if (ZDD) {
6134
6135 if (low == 1) low = univ;
6136 if (high == 1) high = univ;
6137 }
6138
6139 root = bdd_addref(bdd_ite(bdd_ithvar(var), high, low));
6140
6141 loadhash_add(key, root);
6142 }
6143
6144 return root;
6145 }
6146
6147 void loadhash_add(int key, int data) {
6148 int hash = key % lh_nodenum;
6149 int pos = lh_freepos;
6150
6151 lh_freepos = lh_table[pos].next;
6152 lh_table[pos].next = lh_table[hash].first;
6153 lh_table[hash].first = pos;
6154
6155 lh_table[pos].key = key;
6156 lh_table[pos].data = data;
6157 }
6158
6159 int loadhash_get(int key) {
6160 int hash = lh_table[key % lh_nodenum].first;
6161
6162 while (hash != -1 && lh_table[hash].key != key)
6163 hash = lh_table[hash].next;
6164
6165 if (hash == -1)
6166 return -1;
6167 return lh_table[hash].data;
6168 }
6169
6170 void bdd_save(BufferedWriter out, int r) throws IOException {
6171 int[] n = new int[1];
6172
6173 if (r < 2) {
6174 out.write("0 0 " + r + "\n");
6175 return;
6176 }
6177
6178 bdd_markcount(r, n);
6179 bdd_unmark(r);
6180 out.write(n[0] + " " + bddvarnum + "\n");
6181
6182 for (int x = 0; x < bddvarnum; x++)
6183 out.write(bddvar2level[x] + " ");
6184 out.write("\n");
6185
6186 bdd_save_rec(out, r);
6187 bdd_unmark(r);
6188
6189 out.flush();
6190 return;
6191 }
6192
6193
6194 void bdd_save_rec(BufferedWriter out, int root) throws IOException {
6195
6196 if (root < 2)
6197 return;
6198
6199 if (MARKED(root))
6200 return;
6201 SETMARK(root);
6202
6203 bdd_save_rec(out, LOW(root));
6204 bdd_save_rec(out, HIGH(root));
6205
6206 out.write(root + " ");
6207 out.write(bddlevel2var[LEVEL(root)] + " ");
6208 out.write(LOW(root) + " ");
6209 out.write(HIGH(root) + "\n");
6210
6211 return;
6212 }
6213
6214 static String right(int x, int w) {
6215 return right(Integer.toString(x), w);
6216 }
6217 static String right(String s, int w) {
6218 int n = s.length();
6219
6220 StringBuffer b = new StringBuffer(w);
6221 for (int i = n; i < w; ++i) {
6222 b.append(' ');
6223 }
6224 b.append(s);
6225 return b.toString();
6226 }
6227
6228 int bdd_intaddvarblock(int first, int last, boolean fixed) {
6229 BddTree t;
6230
6231 if (first < 0 || first >= bddvarnum || last < 0 || last >= bddvarnum)
6232 return bdd_error(BDD_VAR);
6233
6234 if ((t = bddtree_addrange(vartree, first, last, fixed, blockid))
6235 == null)
6236 return bdd_error(BDD_VARBLK);
6237
6238 vartree = t;
6239 return blockid++;
6240 }
6241
6242 BddTree bddtree_addrange_rec(BddTree t, BddTree prev,
6243 int first, int last, boolean fixed, int id)
6244 {
6245 if (first < 0 || last < 0 || last < first)
6246 return null;
6247
6248
6249 if (t == null) {
6250 t = bddtree_new(id);
6251 t.firstVar = first;
6252 t.firstLevel = bddvar2level[first];
6253 t.fixed = fixed;
6254 t.seq = new int[last - first + 1];
6255 t.lastVar = last;
6256 t.lastLevel = bddvar2level[last];
6257 update_seq(t);
6258 t.prev = prev;
6259 return t;
6260 }
6261
6262
6263 if (first == t.firstVar && last == t.lastVar)
6264 return t;
6265
6266 int firstLev = Math.min(bddvar2level[first], bddvar2level[last]);
6267 int lastLev = Math.max(bddvar2level[first], bddvar2level[last]);
6268
6269
6270 if (firstLev >= t.firstLevel && lastLev <= t.lastLevel) {
6271 t.nextlevel =
6272 bddtree_addrange_rec(t.nextlevel, null, first, last, fixed, id);
6273 return t;
6274 }
6275
6276
6277 if (lastLev < t.firstLevel) {
6278 BddTree tnew = bddtree_new(id);
6279 tnew.firstVar = first;
6280 tnew.firstLevel = firstLev;
6281 tnew.lastVar = last;
6282 tnew.lastLevel = lastLev;
6283 tnew.fixed = fixed;
6284 tnew.seq = new int[last - first + 1];
6285 update_seq(tnew);
6286 tnew.next = t;
6287 tnew.prev = t.prev;
6288 t.prev = tnew;
6289 return tnew;
6290 }
6291
6292
6293 if (firstLev > t.lastLevel) {
6294 t.next = bddtree_addrange_rec(t.next, t, first, last, fixed, id);
6295 return t;
6296 }
6297
6298
6299 if (firstLev <= t.firstLevel) {
6300 BddTree tnew;
6301 BddTree dis = t;
6302
6303 while (true) {
6304
6305 if (lastLev >= dis.firstLevel && lastLev < dis.lastLevel)
6306 return null;
6307
6308 if (dis.next == null || last < dis.next.firstLevel) {
6309 tnew = bddtree_new(id);
6310 tnew.firstVar = first;
6311 tnew.firstLevel = firstLev;
6312 tnew.lastVar = last;
6313 tnew.lastLevel = lastLev;
6314 tnew.fixed = fixed;
6315 tnew.seq = new int[last - first + 1];
6316 update_seq(tnew);
6317 tnew.nextlevel = t;
6318 tnew.next = dis.next;
6319 tnew.prev = t.prev;
6320 if (dis.next != null)
6321 dis.next.prev = tnew;
6322 dis.next = null;
6323 t.prev = null;
6324 return tnew;
6325 }
6326
6327 dis = dis.next;
6328 }
6329
6330 }
6331
6332 return null;
6333 }
6334
6335 void update_seq(BddTree t) {
6336 int n;
6337 int low = t.firstVar;
6338 int high = t.lastVar;
6339
6340 for (n = t.firstVar; n <= t.lastVar; n++) {
6341 if (bddvar2level[n] < bddvar2level[low])
6342 low = n;
6343 if (bddvar2level[n] > bddvar2level[high])
6344 high = n;
6345 }
6346
6347 for (n = t.firstVar; n <= t.lastVar; n++)
6348 t.seq[bddvar2level[n] - bddvar2level[low]] = n;
6349
6350 t.firstLevel = bddvar2level[low];
6351 t.lastLevel = bddvar2level[high];
6352 }
6353
6354 BddTree bddtree_addrange(BddTree t, int first, int last, boolean fixed, int id) {
6355 return bddtree_addrange_rec(t, null, first, last, fixed, id);
6356 }
6357
6358 void bdd_varblockall() {
6359 int n;
6360
6361 for (n = 0; n < bddvarnum; n++)
6362 bdd_intaddvarblock(n, n, true);
6363 }
6364
6365 void print_order_rec(PrintStream o, BddTree t, int level) {
6366 if (t == null)
6367 return;
6368
6369 if (t.nextlevel != null) {
6370 for (int i = 0; i < level; ++i)
6371 o.print(" ");
6372
6373 o.print(right(t.id, 3));
6374 if (t.interleaved) o.print('x');
6375 o.println("{\n");
6376
6377 print_order_rec(o, t.nextlevel, level + 1);
6378
6379 for (int i = 0; i < level; ++i)
6380 o.print(" ");
6381
6382 o.print(right(t.id, 3));
6383 o.println("}\n");
6384
6385 print_order_rec(o, t.next, level);
6386 } else {
6387 for (int i = 0; i < level; ++i)
6388 o.print(" ");
6389
6390 o.print(right(t.id, 3));
6391 if (t.interleaved) o.print('x');
6392 o.println();
6393
6394 print_order_rec(o, t.next, level);
6395 }
6396 }
6397
6398 void bdd_fprintorder(PrintStream ofile) {
6399 print_order_rec(ofile, vartree, 0);
6400 }
6401
6402 void bdd_fprintstat(PrintStream out) {
6403 CacheStats s = cachestats;
6404 out.print(s.toString());
6405 }
6406
6407 void bdd_validate_all() {
6408 int n;
6409 for (n = bddnodesize - 1; n >= 2; n--) {
6410 if (HASREF(n)) {
6411 bdd_validate(n);
6412 }
6413 }
6414 }
6415 void bdd_validate(int k) {
6416 try {
6417 validate(k, -1);
6418 } finally {
6419 bdd_unmark(k);
6420 }
6421 }
6422 void validate(int k, int lastLevel) {
6423 if (k < 2) return;
6424 int lev = LEVEL(k);
6425
6426 if (lev <= lastLevel)
6427 throw new BDDException(lev+" <= "+lastLevel);
6428 if (ZDD) {
6429 if (HIGH(k) == 0)
6430 throw new BDDException("HIGH("+k+")==0");
6431 } else {
6432 if (LOW(k) == HIGH(k))
6433 throw new BDDException("LOW("+k+") == HIGH("+k+")");
6434 }
6435 if (MARKED(k)) return;
6436 SETMARK(k);
6437
6438 validate(LOW(k), lev);
6439
6440 validate(HIGH(k), lev);
6441 }
6442
6443
6444
6445 Random rng = new Random();
6446
6447 final int Random(int i) {
6448 return rng.nextInt(i) + 1;
6449 }
6450
6451 static boolean isEven(int src) {
6452 return (src & 0x1) == 0;
6453 }
6454
6455 static boolean hasFactor(int src, int n) {
6456 return (src != n) && (src % n == 0);
6457 }
6458
6459 static boolean BitIsSet(int src, int b) {
6460 return (src & (1 << b)) != 0;
6461 }
6462
6463 static final int CHECKTIMES = 20;
6464
6465 static final int u64_mulmod(int a, int b, int c) {
6466 return (int) (((long) a * (long) b) % (long) c);
6467 }
6468
6469 /**************************************************************************
6470 Miller Rabin check
6471 *************************************************************************/
6472
6473 static int numberOfBits(int src) {
6474 int b;
6475
6476 if (src == 0)
6477 return 0;
6478
6479 for (b = 31; b > 0; --b)
6480 if (BitIsSet(src, b))
6481 return b + 1;
6482
6483 return 1;
6484 }
6485
6486 static boolean isWitness(int witness, int src) {
6487 int bitNum = numberOfBits(src - 1) - 1;
6488 int d = 1;
6489 int i;
6490
6491 for (i = bitNum; i >= 0; --i) {
6492 int x = d;
6493
6494 d = u64_mulmod(d, d, src);
6495
6496 if (d == 1 && x != 1 && x != src - 1)
6497 return true;
6498
6499 if (BitIsSet(src - 1, i))
6500 d = u64_mulmod(d, witness, src);
6501 }
6502
6503 return d != 1;
6504 }
6505
6506 boolean isMillerRabinPrime(int src) {
6507 int n;
6508
6509 for (n = 0; n < CHECKTIMES; ++n) {
6510 int witness = Random(src - 1);
6511
6512 if (isWitness(witness, src))
6513 return false;
6514 }
6515
6516 return true;
6517 }
6518
6519 /**************************************************************************
6520 Basic prime searching stuff
6521 *************************************************************************/
6522
6523 static boolean hasEasyFactors(int src) {
6524 return hasFactor(src, 3)
6525 || hasFactor(src, 5)
6526 || hasFactor(src, 7)
6527 || hasFactor(src, 11)
6528 || hasFactor(src, 13);
6529 }
6530
6531 boolean isPrime(int src) {
6532 if (hasEasyFactors(src))
6533 return false;
6534
6535 return isMillerRabinPrime(src);
6536 }
6537
6538 /**************************************************************************
6539 External interface
6540 *************************************************************************/
6541
6542 int bdd_prime_gte(int src) {
6543 if (isEven(src))
6544 ++src;
6545
6546 while (!isPrime(src))
6547 src += 2;
6548
6549 return src;
6550 }
6551
6552 int bdd_prime_lte(int src) {
6553 if (isEven(src))
6554 --src;
6555
6556 while (!isPrime(src))
6557 src -= 2;
6558
6559 return src;
6560 }
6561
6562 }